V8.7 (#36)

Port SMTCoq to Coq-8.7

2 files changed, 28 insertions, 3 deletions

diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml
index c286f56..dbf3d62 100644
--- a/src/versions/native/structures.ml
+++ b/src/versions/native/structures.ml
@@ -114,6 +114,8 @@ let assert_before = Tactics.assert_tac
 
 let vm_conv = Reduction.vm_conv
 let vm_cast_no_check = Tactics.vm_cast_no_check
+let cbv_vm = Vnorm.cbv_vm
+
 let mk_tactic tac gl =
   let env = Tacmach.pf_env gl in
   let sigma = Tacmach.project gl in
@@ -128,15 +130,28 @@ let constrextern_extern_constr =
 
 let get_rel_dec_name = fun _ -> Names.Anonymous
 
+(* Eta-expanded to get rid of optional arguments *)
+let retyping_get_type_of env = Retyping.get_type_of env
+
 
-(* Old packaging of plugins *)
+(* Micromega *)
 module Micromega_plugin_Certificate = Certificate
 module Micromega_plugin_Coq_micromega = Coq_micromega
 module Micromega_plugin_Micromega = Micromega
 module Micromega_plugin_Mutils = Mutils
 
+let micromega_coq_proofTerm =
+  Coq_micromega.M.coq_proofTerm
+
+let micromega_dump_proof_term p =
+  Coq_micromega.dump_proof_term p
+
 
 (* Types in the Coq source code *)
 type tactic = Proof_type.tactic
 type names_id = Names.identifier
 type constr_expr = Topconstr.constr_expr
+
+(* EConstr *)
+type econstr = Term.constr
+let econstr_of_constr e = e
diff --git a/src/versions/native/structures.mli b/src/versions/native/structures.mli
index b4d9731..9ec21d2 100644
--- a/src/versions/native/structures.mli
+++ b/src/versions/native/structures.mli
@@ -24,7 +24,6 @@ val mkTrace :
   'b ->
   'c -> 'd -> 'e -> int -> Term.types -> Term.constr -> 'a ref -> Term.constr
 type names_id_t = Names.identifier
-val dummy_loc : Pp.loc
 val mkUConst : Term.constr -> Entries.definition_entry
 val mkTConst : Term.constr -> 'a -> Term.types -> Entries.definition_entry
 val error : string -> 'a
@@ -40,8 +39,11 @@ val interp_constr : Environ.env -> Evd.evar_map -> Topconstr.constr_expr -> Term
 val tclTHEN : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic
 val tclTHENLAST : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic
 val assert_before : Names.name -> Term.types -> Proof_type.tactic
+
 val vm_conv : Reduction.conv_pb -> Term.types Reduction.conversion_function
 val vm_cast_no_check : Term.constr -> Proof_type.tactic
+val cbv_vm : Environ.env -> Term.constr -> Term.types -> Term.constr
+
 val mk_tactic :
   (Environ.env ->
    Evd.evar_map -> Term.types -> Proof_type.goal Tacmach.sigma -> 'a) ->
@@ -50,16 +52,24 @@ val set_evars_tac : 'a -> Proof_type.tactic
 val ppconstr_lsimpleconstr : Ppconstr.precedence
 val constrextern_extern_constr : Term.constr -> Topconstr.constr_expr
 val get_rel_dec_name : 'a -> Names.name
+val retyping_get_type_of : Environ.env -> Evd.evar_map -> Term.constr -> Term.constr
 
 
-(* Old packaging of plugins *)
+(* Micromega *)
 module Micromega_plugin_Certificate = Certificate
 module Micromega_plugin_Coq_micromega = Coq_micromega
 module Micromega_plugin_Micromega = Micromega
 module Micromega_plugin_Mutils = Mutils
 
+val micromega_coq_proofTerm : Term.constr lazy_t
+val micromega_dump_proof_term : Micromega_plugin_Certificate.Mc.zArithProof -> Term.constr
+
 
 (* Types in the Coq source code *)
 type tactic = Proof_type.tactic
 type names_id = Names.identifier
 type constr_expr = Topconstr.constr_expr
+
+(* EConstr *)
+type econstr = Term.constr
+val econstr_of_constr : Term.constr -> econstr