Support Coq 8.11

.gitignore

@@ -5,8 +5,11 @@
 *.d
 /Makefile
 Makefile.conf
+g_coq_cw.ml
 .merlin
 *.vo
+*.vok
+*.vos
 *.glob
 *.aux
 *.cmi

_CoqProject

@@ -5,5 +5,5 @@ theories/Loader.v
 
 src/coq_cw.ml
 src/coq_cw.mli
-src/g_coq_cw.ml4
+src/g_coq_cw.mlg
 src/coq_cw_plugin.mlpack

src/coq_cw.ml

@@ -92,7 +92,7 @@ let locate_constant r =
   try
     let gr = Smartlocate.locate_global_with_alias r in
     match gr with
-    | Globnames.ConstRef cst -> cst
+    | Names.GlobRef.ConstRef cst -> cst
     | _ -> CErrors.user_err (str "A constant is expected: " ++ Printer.pr_global gr)
   with Not_found -> CErrors.user_err (str "Not found: " ++ Libnames.pr_qualid r)
 

src/g_coq_cw.ml4 → src/g_coq_cw.mlg

@@ -1,69 +1,73 @@
 DECLARE PLUGIN "coq_cw_plugin"
 
+{
+
 open Stdarg
 
+}
+
 VERNAC COMMAND EXTEND CWAssertType CLASSIFIED AS QUERY
-| [ "CWAssert" string_opt(msg) ref(r) ":" constr(ty)] -> [ 
+| [ "CWAssert" string_opt(msg) ref(r) ":" constr(ty)] -> { 
         Coq_cw.test_type ?msg r ty
-    ]
+    }
 END
 
 VERNAC COMMAND EXTEND CWAssertAssumptions CLASSIFIED AS QUERY
-| [ "CWAssert" string_opt(msg) ref(e) "Assumes" ref_list(axioms)] -> [ 
+| [ "CWAssert" string_opt(msg) ref(e) "Assumes" ref_list(axioms)] -> { 
         Coq_cw.test_axioms ?msg e axioms
-    ]
+    }
 END
 
 VERNAC COMMAND EXTEND CWStopOnFailure CLASSIFIED AS SIDEFF
-| [ "CWStopOnFailure" int(flag)] -> [
+| [ "CWStopOnFailure" int(flag)] -> {
         Coq_cw.stop_on_failure flag
-    ]
+    }
 END
 
 VERNAC COMMAND EXTEND CWGroup CLASSIFIED AS SIDEFF
-| [ "CWGroup" string(msg)] -> [ 
+| [ "CWGroup" string(msg)] -> {
         Coq_cw.begin_group "DESCRIBE" msg
-    ]
+    }
 END
 
 VERNAC COMMAND EXTEND CWEndGroup CLASSIFIED AS SIDEFF
-| [ "CWEndGroup"] -> [
+| [ "CWEndGroup"] -> {
         Coq_cw.end_group "DESCRIBE"
-    ]
+    }
 END
 
 VERNAC COMMAND EXTEND CWTest CLASSIFIED AS SIDEFF
-| [ "CWTest" string(msg)] -> [ 
+| [ "CWTest" string(msg)] -> {
         Coq_cw.begin_group "IT" msg
-    ]
+    }
 END
 
 VERNAC COMMAND EXTEND CWEndTest CLASSIFIED AS SIDEFF
-| [ "CWEndTest"] -> [
+| [ "CWEndTest"] -> {
         Coq_cw.end_group "IT"
-    ]
+    }
 END
 
 VERNAC COMMAND EXTEND CWFileSize CLASSIFIED AS QUERY
-| [ "CWFile" string_opt(fname) "Size" "<" int(size)] -> [ 
+| [ "CWFile" string_opt(fname) "Size" "<" int(size)] -> {
         Coq_cw.test_file_size ?fname size
-    ]
+    }
 END
 
 VERNAC COMMAND EXTEND CWFileMatch CLASSIFIED AS QUERY
-| [ "CWFile" string_opt(fname) "Matches" string(regex)] -> [ 
+| [ "CWFile" string_opt(fname) "Matches" string(regex)] -> {
         Coq_cw.test_file_regex ?fname true regex
-    ]
+    }
 END
 
 VERNAC COMMAND EXTEND CWFileNegMatch CLASSIFIED AS QUERY
-| [ "CWFile" string_opt(fname) "Does" "Not" "Match" string(regex)] -> [ 
+| [ "CWFile" string_opt(fname) "Does" "Not" "Match" string(regex)] -> {
         Coq_cw.test_file_regex ?fname false regex
-    ]
+    }
 END
 
-VERNAC COMMAND EXTEND CWCompileAndRun CLASSIFIED AS SIDEFF
-| [ "CWCompileAndRun" string_list(files) "Options" string_opt(options) "Driver" string(driver) ] -> [
+VERNAC COMMAND EXTEND CWCompileAndRun CLASSIFIED AS QUERY
+| [ "CWCompileAndRun" string_list(files) "Options" string_opt(options) "Driver" string(driver) ] -> {
         Coq_cw.compile_and_run files ?options driver
-    ]
+    }
 END

theories/Demo2.v

@@ -52,12 +52,17 @@ Print Assumptions sqrt_pos.
 CWGroup "Real numbers".
 
 Fail CWAssert sqrt_pos Assumes.
-CWAssert "Real Number Axioms" sqrt_pos Assumes
+CWAssert "Real Number Axioms (Dedekind)" sqrt_pos Assumes
+  ClassicalDedekindReals.sig_not_dec
+  ClassicalDedekindReals.sig_forall_dec
+  functional_extensionality_dep.
+
+(* CWAssert "Real Number Axioms" sqrt_pos Assumes
   R R0 R1 Rplus Rmult Ropp Rinv Rlt up
   Rplus_comm Rplus_assoc Rplus_opp_r Rplus_0_l
   Rmult_comm Rmult_assoc Rinv_l Rmult_1_l R1_neq_R0
   Rmult_plus_distr_l total_order_T
   Rlt_asym Rlt_trans Rplus_lt_compat_l Rmult_lt_compat_l
-  archimed completeness.  
+  archimed completeness.   *)
 
 CWEndGroup.