Compiles with Coq 8.4

Makefile.in

@@ -785,9 +785,9 @@ endif
 
 ifeq (@enable_coq_plugin@,yes)
 
-COQPGENERATED = src/coq-tactic/g_why3tac.ml
+COQPGENERATED = src/coq-tactic/coqCompat.ml src/coq-tactic/g_why3tac.ml
 
-COQP_FILES = why3tac g_why3tac
+COQP_FILES = coqCompat why3tac g_why3tac
 
 COQPMODULES = $(addprefix src/coq-tactic/, $(COQP_FILES))
 
@@ -806,6 +806,10 @@ $(COQPDEP): $(COQPGENERATED)
 byte: src/coq-tactic/.why3-vo-byte
 opt:  src/coq-tactic/.why3-vo-opt
 
+src/coq-tactic/coqCompat.cmo:  BFLAGS+=-rectypes 
+src/coq-tactic/coqCompat.cmx: OFLAGS+=-rectypes 
+src/coq-tactic/why3tac.cmo:  BFLAGS+=-rectypes -I +camlp5
+src/coq-tactic/why3tac.cmx:  BFLAGS+=-rectypes -I +camlp5
 lib/coq-tactic/why3tac.cma:  BFLAGS+=-rectypes -I +camlp5
 lib/coq-tactic/why3tac.cmxs: OFLAGS+=-rectypes -I +camlp5
 

configure.in

@@ -389,13 +389,14 @@ else
         COQVERSION=`$COQC -v | sed -n -e 's|.*version* *\([[^ ]]*\) .*$|\1|p' `
 
         case $COQVERSION in
-          8.0*|8.1*|8.2*)
-                enable_coq_support=no
-                AC_MSG_WARN(You need Coq 8.3 or later; Coq discarded)
-                reason_coq_support=" (need version 8.3 or later)"
+          8.3*)
+	        enable_coq_support=yes
+                cp -f src/coq-tactic/coqCompat.8.3.ml src/coq-tactic/coqCompat.ml
+                AC_MSG_RESULT($COQVERSION)
                 ;;
           8.*|trunk)
 	        enable_coq_support=yes
+                cp -f src/coq-tactic/coqCompat.8.4.ml src/coq-tactic/coqCompat.ml
                 AC_MSG_RESULT($COQVERSION)
                 ;;
           *)

src/coq-tactic/coqCompat.8.3.ml

+
+let body_of_constant c = c.const_body

src/coq-tactic/coqCompat.8.4.ml

+
+let body_of_constant = Declarations.body_of_constant

src/coq-tactic/coqCompat.mli

+
+val body_of_constant :
+  Declarations.constant_body -> Declarations.constr_substituted option

src/coq-tactic/why3tac.ml

@@ -19,7 +19,6 @@
 (**************************************************************************)
 
 open Names
-open Nameops
 open Namegen
 open Term
 open Termops
@@ -504,7 +503,7 @@ and tr_global_ts dep env r =
           let (_,vars), _, t = decomp_type_quantifiers env ty in
           if not (is_Set t) && not (is_Type t) then raise NotFO;
           let id = preid_of_id (Nametab.basename_of_global r) in
-          let ts = match (Global.lookup_constant c).const_body with
+          let ts = match CoqCompat.body_of_constant (Global.lookup_constant c) with
             | Some b ->
                 let b = force b in
                 let tvm, env, t = decomp_type_lambdas Idmap.empty env vars b in
@@ -652,7 +651,7 @@ and make_one_ls dep env r =
   add_poly_arity ls vars
 
 and decompose_definition dep env c =
-  let dl = match (Global.lookup_constant c).const_body with
+  let dl = match CoqCompat.body_of_constant (Global.lookup_constant c) with
     | None ->
         [ConstRef c, None]
     | Some b ->
@@ -1126,8 +1125,10 @@ let tr_top_decl = function
   | _, Lib.CompilingLibrary _
   | _, Lib.OpenedModule _
   | _, Lib.ClosedModule  _
+(*
   | _, Lib.OpenedModtype _
   | _, Lib.ClosedModtype _
+*)
   | _, Lib.OpenedSection _
   | _, Lib.ClosedSection _
   | _, Lib.FrozenState _ -> ()