2 files changed, 24 insertions, 2 deletions
diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml
index 62907d1..919f2f1 100644
--- a/src/versions/native/structures.ml
+++ b/src/versions/native/structures.ml
@@ -41,6 +41,8 @@ let mkArray : Term.types * Term.constr array -> Term.constr =
 
 
 (* Differences between the two versions of Coq *)
+type names_id_t = Names.identifier
+
 let dummy_loc = Pp.dummy_loc
 
 let mkConst c =
@@ -71,4 +73,12 @@ let pr_constr_env = Printer.pr_constr_env
 
 let lift = Term.lift
 
-let mk_tactic t = t
+let mk_sat_tactic tac = tac
+let tclTHENLAST = Tacticals.tclTHENLAST
+let assert_before = Tactics.assert_tac
+let vm_cast_no_check = Tactics.vm_cast_no_check
+let mk_smt_tactic tac gl =
+  let env = Tacmach.pf_env gl in
+  let sigma = Tacmach.project gl in
+  let t = Tacmach.pf_concl gl in
+  tac env sigma t gl
diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml
index 93546b3..66106a6 100644
--- a/src/versions/standard/structures.ml
+++ b/src/versions/standard/structures.ml
@@ -64,6 +64,8 @@ let mkArray : Term.types * Term.constr array -> Term.constr =
 
 
 (* Differences between the two versions of Coq *)
+type names_id_t = Names.Id.t
+
 let dummy_loc = Loc.ghost
 
 let mkConst c =
@@ -101,4 +103,14 @@ let pr_constr_env env = Printer.pr_constr_env env Evd.empty
 
 let lift = Vars.lift
 
-let mk_tactic = Proofview.V82.tactic
+let mk_sat_tactic = Proofview.V82.tactic
+let tclTHENLAST = Tacticals.New.tclTHENLAST
+let assert_before = Tactics.assert_before
+let vm_cast_no_check t = Proofview.V82.tactic (Tactics.vm_cast_no_check t)
+let mk_smt_tactic tac =
+  Proofview.Goal.nf_enter (fun gl ->
+    let env = Proofview.Goal.env gl in
+    let sigma = Proofview.Goal.sigma gl in
+    let t = Proofview.Goal.concl gl in
+    tac env sigma t
+  )