diff options
Diffstat (limited to 'plugins/btauto')
| -rw-r--r-- | plugins/btauto/g_btauto.ml4 | 2 | ||||
| -rw-r--r-- | plugins/btauto/refl_btauto.ml | 2 |
2 files changed, 3 insertions, 1 deletions
diff --git a/plugins/btauto/g_btauto.ml4 b/plugins/btauto/g_btauto.ml4 index f3e2c99f4c..2980274487 100644 --- a/plugins/btauto/g_btauto.ml4 +++ b/plugins/btauto/g_btauto.ml4 @@ -8,6 +8,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +open Ltac_plugin + DECLARE PLUGIN "btauto_plugin" TACTIC EXTEND btauto diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 6e8b2eb0fb..2c5b108e55 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -15,7 +15,7 @@ let get_inductive dir s = Lazy.from_fun (fun () -> Globnames.destIndRef (glob_ref ())) let decomp_term (c : Term.constr) = - Term.kind_of_term (Term.strip_outer_cast c) + Term.kind_of_term (Termops.strip_outer_cast c) let lapp c v = Term.mkApp (Lazy.force c, v) |