From 79f84f5e5b82240cbaaa761548f9d6614c552006 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 2 Dec 2019 17:05:51 +0100
Subject: [PATCH] [WP+Coq] CodIDE 8.10 compatibility
---
src/plugins/wp/ProverCoq.ml | 9 +--------
1 file changed, 1 insertion(+), 8 deletions(-)
diff --git a/src/plugins/wp/ProverCoq.ml b/src/plugins/wp/ProverCoq.ml
index e119809bcc5..946fc35b9cc 100644
--- a/src/plugins/wp/ProverCoq.ml
+++ b/src/plugins/wp/ProverCoq.ml
@@ -401,7 +401,7 @@ class runcoq includes source =
else
Format.fprintf fmt "-R %s %s@\n" dir name
) includes ;
- Format.fprintf fmt "-arg -noglob@\n" ;
+ Format.fprintf fmt "-arg@\n" ;
end
method private options =
@@ -413,7 +413,6 @@ class runcoq includes source =
else
self#add ["-R";dir;name]
) includes ;
- self#add [ "-noglob" ] ;
end
method failed : 'a. 'a task =
@@ -458,24 +457,18 @@ class runcoq includes source =
| 1 -> Task.return false
| _ -> self#failed
- method script =
- let script = Wp_parameters.Script.get () in
- if Sys.file_exists script then self#add [ script ]
-
method coqide =
let coqide = Wp_parameters.CoqIde.get () in
self#set_command coqide ;
if is_emacs coqide then
begin
self#project ;
- self#script ;
self#add [ source ] ;
end
else
begin
self#options ;
self#add [ source ] ;
- self#script ;
end ;
Task.sync coqide_lock (self#run ~logout ~logerr)
end
--
GitLab