diff options
Diffstat (limited to 'plugins/btauto')
| -rw-r--r-- | plugins/btauto/btauto_plugin.mlpack (renamed from plugins/btauto/btauto_plugin.mllib) | 1 | ||||
| -rw-r--r-- | plugins/btauto/refl_btauto.ml | 4 |
2 files changed, 2 insertions, 3 deletions
diff --git a/plugins/btauto/btauto_plugin.mllib b/plugins/btauto/btauto_plugin.mlpack index 319a9c302a..2410f906a3 100644 --- a/plugins/btauto/btauto_plugin.mllib +++ b/plugins/btauto/btauto_plugin.mlpack @@ -1,3 +1,2 @@ Refl_btauto G_btauto -Btauto_plugin_mod diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index aee0bd8564..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) @@ -212,7 +212,7 @@ module Btauto = struct let assign = List.map map_msg assign in let l = str "[" ++ (concat (str ";" ++ spc ()) assign) ++ str "]" in str "Not a tautology:" ++ spc () ++ l - with e when Errors.noncritical e -> (str "Not a tautology") + with e when CErrors.noncritical e -> (str "Not a tautology") in Tacticals.tclFAIL 0 msg gl |