diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-09-28 15:33:17 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-09-28 15:33:17 +0200 |
| commit | b3f7d3361fac0d1771e6ea3eb277ad858ce38760 (patch) | |
| tree | fdf80fcee557857bf70912f2b98831a53b3be8ad /src/versions/native | |
| parent | 73e19ad0aac3cbd472b8add74594bbc158fce334 (diff) | |
| download | smtcoq-b3f7d3361fac0d1771e6ea3eb277ad858ce38760.tar.gz smtcoq-b3f7d3361fac0d1771e6ea3eb277ad858ce38760.zip | |
Hopefully solved the problem with universes for the tactic
Diffstat (limited to 'src/versions/native')
| -rw-r--r-- | src/versions/native/structures.ml | 2 |
1 files changed, 2 insertions, 0 deletions
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 = |