From b3f7d3361fac0d1771e6ea3eb277ad858ce38760 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Wed, 28 Sep 2016 15:33:17 +0200 Subject: Hopefully solved the problem with universes for the tactic --- src/versions/native/structures.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/versions/native') diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml index f6b21c8..9a56d43 100644 --- a/src/versions/native/structures.ml +++ b/src/versions/native/structures.ml @@ -108,6 +108,7 @@ let pr_constr_env = Printer.pr_constr_env let lift = Term.lift +let tclTHEN = Tacticals.tclTHEN let tclTHENLAST = Tacticals.tclTHENLAST let assert_before = Tactics.assert_tac let vm_cast_no_check = Tactics.vm_cast_no_check @@ -116,6 +117,7 @@ let mk_tactic tac gl = let sigma = Tacmach.project gl in let t = Tacmach.pf_concl gl in tac env sigma t gl +let set_evars_tac _ = Tacticals.tclIDTAC let ppconstr_lsimpleconstr = Ppconstr.lsimple let constrextern_extern_constr = -- cgit