From 4a610de645ca2bb505c97dd082220a57595019ad Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@inria.fr>
Date: Tue, 12 Mar 2019 09:52:17 +0100
Subject: Support for native-coq

---
 src/versions/native/structures.ml  | 11 ++++++++---
 src/versions/native/structures.mli | 12 ++++++------
 2 files changed, 14 insertions(+), 9 deletions(-)

(limited to 'src')

diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml
index 13beb9d..e11697e 100644
--- a/src/versions/native/structures.ml
+++ b/src/versions/native/structures.ml
@@ -15,7 +15,7 @@ open Coqlib
 
 
 (* Constr generation and manipulation *)
-type id = Names.id
+type id = Names.identifier
 let mkId = Names.id_of_string
 
 
@@ -34,7 +34,7 @@ type types = Term.types
 let eq_constr = Term.eq_constr
 let hash_constr = Term.hash_constr
 let mkProp = Term.mkProp
-let mkConst = Constr.mkConst
+let mkConst = Term.mkConst
 let mkVar = Term.mkVar
 let mkRel = Term.mkRel
 let isRel = Term.isRel
@@ -49,6 +49,9 @@ let mkLetIn = Term.mkLetIn
 let pr_constr_env = Printer.pr_constr_env
 let pr_constr = Printer.pr_constr
 
+
+let dummy_loc = Pp.dummy_loc
+
 let mkUConst c =
   { const_entry_body = c;
     const_entry_type = None;
@@ -65,7 +68,7 @@ let mkTConst c _ ty =
 
 (* TODO : Set -> Type *)
 let declare_new_type t =
-  Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) (Lazy.force Term.mkSet) [] false None (dummy_loc, t);
+  Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) Term.mkSet [] false None (dummy_loc, t);
   Term.mkVar t
 
 let declare_new_variable v constr_t =
@@ -149,6 +152,7 @@ let micromega_dump_proof_term p =
 
 
 (* Tactics *)
+type tactic = Proof_type.tactic
 let tclTHEN = Tacticals.tclTHEN
 let tclTHENLAST = Tacticals.tclTHENLAST
 let assert_before = Tactics.assert_tac
@@ -162,6 +166,7 @@ let set_evars_tac _ = Tacticals.tclIDTAC
 
 
 (* Other differences between the two versions of Coq *)
+type constr_expr = Topconstr.constr_expr
 let error = Errors.error
 let extern_constr = Constrextern.extern_constr true Environ.empty_env
 let destruct_rel_decl (n, _, t) = n, t
diff --git a/src/versions/native/structures.mli b/src/versions/native/structures.mli
index abedc17..cae581e 100644
--- a/src/versions/native/structures.mli
+++ b/src/versions/native/structures.mli
@@ -11,7 +11,7 @@
 
 
 (* Constr generation and manipulation *)
-type id
+type id = Names.variable
 val mkId : string -> id
 
 type name
@@ -24,26 +24,26 @@ type types = constr
 val eq_constr : constr -> constr -> bool
 val hash_constr : constr -> int
 val mkProp : types
-val mkConst : Names.Constant.t -> constr
+val mkConst : Names.constant -> constr
 val mkVar : id -> constr
 val mkRel : int -> constr
 val isRel : constr -> bool
 val destRel : constr -> int
 val lift : int -> constr -> constr
-val mkApp : constr -> constr array -> constr
+val mkApp : constr * constr array -> constr
 val decompose_app : constr -> constr * constr list
 val mkLambda : name * types * constr -> constr
 val mkProd : name * types * types -> types
 val mkLetIn : name * constr * types * constr -> constr
 
-val pr_constr_env : Environ.env -> constr -> Pp.t
-val pr_constr : constr -> Pp.t
+val pr_constr_env : Environ.env -> constr -> Pp.std_ppcmds
+val pr_constr : constr -> Pp.std_ppcmds
 
 val mkUConst : constr -> Entries.definition_entry
 val mkTConst : constr -> 'a -> types -> Entries.definition_entry
 val declare_new_type : id -> types
 val declare_new_variable : id -> types -> constr
-val declare_constant : id -> Safe_typing.private_constants Entries.definition_entry -> Names.Constant.t
+val declare_constant : id -> Entries.definition_entry -> Names.constant
 
 type cast_kind
 val vmcast : cast_kind
-- 
cgit