From 499a11a45b5711d4eaabe84a80f0ad3ae539d500 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 8 May 2013 17:47:10 +0200 Subject: Imported Upstream version 8.4pl2dfsg --- proofs/evar_refiner.ml | 2 +- proofs/goal.ml | 16 +++++++++++----- proofs/goal.mli | 2 +- proofs/logic.ml | 2 +- proofs/pfedit.ml | 6 +++--- proofs/proof.ml | 10 +++++----- proofs/proofview.ml | 10 ++++++---- proofs/refiner.ml | 8 ++++---- proofs/tactic_debug.ml | 8 ++++---- 9 files changed, 36 insertions(+), 28 deletions(-) (limited to 'proofs') diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 4462062c..f271a6bd 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -42,7 +42,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = let sigma',typed_c = try Pretyping.Default.understand_ltac ~resolve_classes:true true sigma env ltac_var (Pretyping.OfType (Some evi.evar_concl)) rawc - with _ -> + with e when Errors.noncritical e -> let loc = Glob_term.loc_of_glob_constr rawc in user_err_loc (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^ diff --git a/proofs/goal.ml b/proofs/goal.ml index dc1ac5dd..37ebce67 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -276,7 +276,7 @@ let check_typability env sigma c = let recheck_typability (what,id) env sigma t = try check_typability env sigma t - with _ -> + with e when Errors.noncritical e -> let s = match what with | None -> "the conclusion" | Some id -> "hypothesis "^(Names.string_of_id id) in @@ -474,7 +474,7 @@ module V82 = struct (* Old style hyps primitive *) let hyps evars gl = let evi = content evars gl in - evi.Evd.evar_hyps + Evd.evar_filtered_hyps evi (* Access to ".evar_concl" *) let concl evars gl = @@ -554,10 +554,16 @@ module V82 = struct with a good implementation of them. *) - (* Used for congruence closure *) - let new_goal_with sigma gl new_hyps = + (* Used for congruence closure and change *) + let new_goal_with sigma gl extra_hyps = let evi = content sigma gl in - let new_evi = { evi with Evd.evar_hyps = new_hyps } in + let hyps = evi.Evd.evar_hyps in + let new_hyps = + List.fold_right Environ.push_named_context_val extra_hyps hyps in + let extra_filter = List.map (fun _ -> true) extra_hyps in + let new_filter = extra_filter @ evi.Evd.evar_filter in + let new_evi = + { evi with Evd.evar_hyps = new_hyps; Evd.evar_filter = new_filter } in let new_evi = Typeclasses.mark_unresolvable new_evi in let evk = Evarutil.new_untyped_evar () in let new_sigma = Evd.add Evd.empty evk new_evi in diff --git a/proofs/goal.mli b/proofs/goal.mli index 9cd439ab..c0a094d3 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -232,7 +232,7 @@ module V82 : sig val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool (* Used for congruence closure *) - val new_goal_with : Evd.evar_map -> goal -> Environ.named_context_val -> goal Evd.sigma + val new_goal_with : Evd.evar_map -> goal -> Sign.named_context -> goal Evd.sigma (* Used by the compatibility layer and typeclasses *) val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map diff --git a/proofs/logic.ml b/proofs/logic.ml index d240c1e1..497ab1fa 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -105,7 +105,7 @@ let clear_hyps sigma ids sign cl = let recheck_typability (what,id) env sigma t = try check_typability env sigma t - with _ -> + with e when Errors.noncritical e -> let s = match what with | None -> "the conclusion" | Some id -> "hypothesis "^(string_of_id id) in diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 45e4a84e..7bac87d2 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -68,7 +68,7 @@ let start_proof id str hyps c ?init_tac ?compute_guard hook = | None -> Proofview.tclUNIT () in try Proof_global.run_tactic tac - with e -> Proof_global.discard_current (); raise e + with reraise -> Proof_global.discard_current (); raise reraise let restart_proof () = undo_todepth 1 @@ -164,9 +164,9 @@ let build_constant_by_tactic id sign typ tac = let _,(const,_,_,_) = cook_proof (fun _ -> ()) in delete_current_proof (); const - with e -> + with reraise -> delete_current_proof (); - raise e + raise reraise let build_by_tactic env typ tac = let id = id_of_string ("temporary_proof"^string_of_int (next())) in diff --git a/proofs/proof.ml b/proofs/proof.ml index a4e556c5..012a4dc1 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -323,7 +323,7 @@ let rec rollback pr = let transaction pr t = init_transaction pr; try t (); commit pr - with e -> rollback pr; raise e + with reraise -> rollback pr; raise reraise (* Focus command (focuses on the [i]th subgoal) *) @@ -429,9 +429,9 @@ let run_tactic env tac pr = let tacticced_proofview = Proofview.apply env tac sp in pr.state <- { pr.state with proofview = tacticced_proofview }; push_undo starting_point pr - with e -> + with reraise -> restore_state starting_point pr; - raise e + raise reraise (*** Commands ***) @@ -476,7 +476,7 @@ module V82 = struct let new_proofview = Proofview.V82.instantiate_evar n com sp in pr.state <- { pr.state with proofview = new_proofview }; push_undo starting_point pr - with e -> + with reraise -> restore_state starting_point pr; - raise e + raise reraise end diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 74e40e3b..d299a520 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -320,10 +320,12 @@ let rec tclDISPATCHGEN null join tacs env = { go = fun sk fk step -> (* takes a tactic which can raise exception and makes it pure by *failing* on with these exceptions. Does not catch anomalies. *) let purify t = - let t' env = { go = fun sk fk step -> try (t env).go (fun x -> sk (Util.Inl x)) fk step - with Util.Anomaly _ as e -> raise e - | e -> sk (Util.Inr e) fk step - } + let t' env = + { go = fun sk fk step -> + try (t env).go (fun x -> sk (Util.Inl x)) fk step + with Util.Anomaly _ as e -> raise e + | e when Errors.noncritical e -> sk (Util.Inr e) fk step + } in tclBIND t' begin function | Util.Inl x -> tclUNIT x diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 37c63644..21b43212 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -255,7 +255,7 @@ let tclORELSE0 t1 t2 g = try t1 g with (* Breakpoint *) - | e -> catch_failerror e; t2 g + | e when Errors.noncritical e -> catch_failerror e; t2 g (* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress, then applies t2 *) @@ -267,7 +267,7 @@ let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2 let tclORELSE_THEN t1 t2then t2else gls = match try Some(tclPROGRESS t1 gls) - with e -> catch_failerror e; None + with e when Errors.noncritical e -> catch_failerror e; None with | None -> t2else gls | Some sgl -> @@ -298,7 +298,7 @@ let ite_gen tcal tac_if continue tac_else gl= try tcal tac_if0 continue gl with (* Breakpoint *) - | e -> catch_failerror e; tac_else0 e gl + | e when Errors.noncritical e -> 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 *) @@ -352,7 +352,7 @@ let tclTIMEOUT n t g = | TacTimeout | Loc.Exc_located(_,TacTimeout) -> restore_timeout (); errorlabstrm "Refiner.tclTIMEOUT" (str"Timeout!") - | e -> restore_timeout (); raise e + | reraise -> restore_timeout (); raise reraise (* Beware: call by need of CAML, g is needed *) let rec tclREPEAT t g = diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index b56cb844..27ab990c 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -140,11 +140,11 @@ let debug_prompt lev g tac f = else (decr skip; run false; if !skip=0 then skipped:=0; DebugOn (lev+1)) in (* What to execute *) try f newlevel - with e -> + with reraise -> skip:=0; skipped:=0; - if Logic.catchable_exception e then - ppnl (str "Level " ++ int lev ++ str ": " ++ !explain_logic_error e); - raise e + if Logic.catchable_exception reraise then + ppnl (str "Level " ++ int lev ++ str ": " ++ !explain_logic_error reraise); + raise reraise (* Prints a constr *) let db_constr debug env c = -- cgit v1.2.3