diff options
Diffstat (limited to 'plugins/btauto')
| -rw-r--r-- | plugins/btauto/refl_btauto.ml | 12 | ||||
| -rw-r--r-- | plugins/btauto/vo.itarget | 3 |
2 files changed, 6 insertions, 9 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index a0b04ce3b5..00e80d041f 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -1,4 +1,4 @@ -open Proofview.Notations +open API let contrib_name = "btauto" @@ -8,7 +8,7 @@ let init_constant dir s = in find_constant contrib_name dir s -let get_constant dir s = lazy (Coqlib.gen_constant contrib_name dir s) +let get_constant dir s = lazy (Universes.constr_of_global @@ Coqlib.coq_reference contrib_name dir s) let get_inductive dir s = let glob_ref () = Coqlib.find_reference contrib_name ("Coq" :: dir) s in @@ -219,7 +219,7 @@ module Btauto = struct Tacticals.tclFAIL 0 msg gl let try_unification env = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let concl = Proofview.Goal.concl gl in let eq = Lazy.force eq in let concl = EConstr.Unsafe.to_constr concl in @@ -232,10 +232,10 @@ module Btauto = struct | _ -> let msg = str "Btauto: Internal error" in Tacticals.New.tclFAIL 0 msg - end } + end let tac = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let concl = Proofview.Goal.concl gl in let concl = EConstr.Unsafe.to_constr concl in let sigma = Tacmach.New.project gl in @@ -262,6 +262,6 @@ module Btauto = struct | _ -> let msg = str "Cannot recognize a boolean equality" in Tacticals.New.tclFAIL 0 msg - end } + end end diff --git a/plugins/btauto/vo.itarget b/plugins/btauto/vo.itarget deleted file mode 100644 index 1f72d3ef22..0000000000 --- a/plugins/btauto/vo.itarget +++ /dev/null @@ -1,3 +0,0 @@ -Algebra.vo -Reflect.vo -Btauto.vo |