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 --- proofs/refiner.ml | 33 +++++++++++++++++---------------- 1 file changed, 17 insertions(+), 16 deletions(-) (limited to 'proofs/refiner.ml') diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 14493458..ea8543b0 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -7,13 +7,13 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Evd open Environ open Proof_type open Logic - +open Context.Named.Declaration let sig_it x = x.it let project x = x.sigma @@ -57,7 +57,7 @@ let tclIDTAC gls = goal_goal_list gls (* the message printing identity tactic *) let tclIDTAC_MESSAGE s gls = - Pp.msg_info (hov 0 s); pp_flush (); tclIDTAC gls + Feedback.msg_info (hov 0 s); tclIDTAC gls (* General failure tactic *) let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s) @@ -197,12 +197,12 @@ let tclNOTSAMEGOAL (tac : tactic) goal = destruct), this is not detected by this tactical. *) let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) :Proof_type.goal list Evd.sigma = - let oldhyps:Context.named_context = pf_hyps goal in + let oldhyps:Context.Named.t = pf_hyps goal in let rslt:Proof_type.goal list Evd.sigma = tac goal in let { it = gls; sigma = sigma; } = rslt in - let hyps:Context.named_context list = + let hyps:Context.Named.t list = List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in - let cmp (i1, c1, t1) (i2, c2, t2) = Names.Id.equal i1 i2 in + let cmp d1 d2 = Names.Id.equal (get_id d1) (get_id d2) in let newhyps = List.map (fun hypl -> List.subtract cmp hypl oldhyps) @@ -215,12 +215,13 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) List.fold_left (fun acc lh -> acc ^ (if !frst then (frst:=false;"") else " | ") ^ (List.fold_left - (fun acc (nm,_,_) -> (Names.Id.to_string nm) ^ " " ^ acc) + (fun acc d -> (Names.Id.to_string (get_id d)) ^ " " ^ acc) "" lh)) "" newhyps in - pp (str (emacs_str "") + Feedback.msg_notice + (str (emacs_str "") ++ (hov 0 (str s)) - ++ (str (emacs_str "")) ++ fnl()); + ++ (str (emacs_str ""))); tclIDTAC goal;; @@ -239,8 +240,8 @@ let tclORELSE0 t1 t2 g = try t1 g with (* Breakpoint *) - | e when Errors.noncritical e -> - let e = Errors.push e in catch_failerror e; t2 g + | e when CErrors.noncritical e -> + let e = CErrors.push e in catch_failerror e; t2 g (* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress, then applies t2 *) @@ -252,8 +253,8 @@ let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2 let tclORELSE_THEN t1 t2then t2else gls = match try Some(tclPROGRESS t1 gls) - with e when Errors.noncritical e -> - let e = Errors.push e in catch_failerror e; None + with e when CErrors.noncritical e -> + let e = CErrors.push e in catch_failerror e; None with | None -> t2else gls | Some sgl -> @@ -283,12 +284,12 @@ let ite_gen tcal tac_if continue tac_else gl= try tac_else gl with - e' when Errors.noncritical e' -> iraise e in + e' when CErrors.noncritical e' -> iraise e in try tcal tac_if0 continue gl with (* Breakpoint *) - | e when Errors.noncritical e -> - let e = Errors.push e in catch_failerror e; tac_else0 e gl + | e when CErrors.noncritical e -> + let e = CErrors.push e in catch_failerror e; tac_else0 e gl (* Try the first tactic and, if it succeeds, continue with the second one, and if it fails, use the third one *) -- cgit v1.2.3