From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- plugins/btauto/refl_btauto.ml | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) (limited to 'plugins/btauto/refl_btauto.ml') diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 57268a9c..6e8b2eb0 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -1,3 +1,4 @@ +open Proofview.Notations let contrib_name = "btauto" @@ -11,7 +12,7 @@ let get_constant dir s = lazy (Coqlib.gen_constant contrib_name dir s) let get_inductive dir s = let glob_ref () = Coqlib.find_reference contrib_name ("Coq" :: dir) s in - Lazy.lazy_from_fun (fun () -> Globnames.destIndRef (glob_ref ())) + Lazy.from_fun (fun () -> Globnames.destIndRef (glob_ref ())) let decomp_term (c : Term.constr) = Term.kind_of_term (Term.strip_outer_cast c) @@ -211,12 +212,12 @@ 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 let try_unification env = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let eq = Lazy.force eq in let t = decomp_term concl in @@ -228,10 +229,10 @@ module Btauto = struct | _ -> let msg = str "Btauto: Internal error" in Tacticals.New.tclFAIL 0 msg - end + end } let tac = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let eq = Lazy.force eq in let bool = Lazy.force Bool.typ in @@ -249,12 +250,12 @@ module Btauto = struct Tacticals.New.tclTHENLIST [ Tactics.change_concl changed_gl; Tactics.apply (Lazy.force soundness); - Proofview.V82.tactic (Tactics.normalise_vm_in_concl); + Tactics.normalise_vm_in_concl; try_unification env ] | _ -> let msg = str "Cannot recognize a boolean equality" in Tacticals.New.tclFAIL 0 msg - end + end } end -- cgit v1.2.3