From 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Thu, 19 Jan 2006 22:34:29 +0000 Subject: Imported Upstream version 8.0pl3 --- proofs/logic.ml | 26 ++++++++++++-------------- proofs/refiner.ml | 16 ++++++++-------- proofs/tacexpr.ml | 6 +++--- 3 files changed, 23 insertions(+), 25 deletions(-) (limited to 'proofs') diff --git a/proofs/logic.ml b/proofs/logic.ml index 3cc44a0f..cefeb8ae 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: logic.ml,v 1.80.2.1 2004/07/16 19:30:49 herbelin Exp $ *) +(* $Id: logic.ml,v 1.80.2.5 2005/12/17 21:15:52 herbelin Exp $ *) open Pp open Util @@ -54,7 +54,8 @@ open Pretype_errors let catchable_exception = function | Util.UserError _ | TypeError _ | RefinerError _ | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ | RefinerError _ | - Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _))) -> true + Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _) | + Indtypes.InductiveError (Indtypes.NotAllowedCaseAnalysis _ ))) -> true | _ -> false let error_cannot_unify (m,n) = @@ -67,16 +68,9 @@ let check = ref false let without_check tac gl = let c = !check in check := false; - let r = tac gl in - check := c; - r + try let r = tac gl in check := c; r with e -> check := c; raise e -let with_check tac gl = - let c = !check in - check := true; - let r = tac gl in - check := c; - r +let with_check = Options.with_option check (************************************************************************) (************************************************************************) @@ -405,9 +399,13 @@ let convert_hyp sign sigma (id,b,bt as d) = apply_to_hyp sign id (fun sign (_,c,ct) _ -> let env = Global.env_of_context sign in - if !check && not (is_conv env sigma bt ct) && - not (option_compare (is_conv env sigma) b c) then - error "convert-hyp rule passed non-converting term"; + if !check && not (is_conv env sigma bt ct) then + (* Just a warning in V8.0bugfix for compatibility *) + msgnl (str "Compatibility warning: Hazardeous change of the type of " ++ pr_id id ++ + str " (not well-typed in current signature)"); + if !check && not (option_compare (is_conv env sigma) b c) then + msgnl (str "Compatibility warning: Hazardeous change of the body of " ++ pr_id id ++ + str " (not well-typed in current signature)"); add_named_decl d sign) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 55f11d52..785e6dd4 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: refiner.ml,v 1.67.2.1 2004/07/16 19:30:49 herbelin Exp $ *) +(* $Id: refiner.ml,v 1.67.2.3 2005/11/04 08:59:30 herbelin Exp $ *) open Pp open Util @@ -188,12 +188,8 @@ let lookup_tactic s = (* refiner r is a tactic applying the rule r *) -let bad_subproof () = - anomalylabstrm "Refiner.refiner" (str"Bad subproof in validation.") - let check_subproof_connection gl spfl = - if not (list_for_all2eq (fun g pf -> g=pf.goal) gl spfl) - then (bad_subproof (); false) else true + list_for_all2eq (fun g pf -> g=pf.goal) gl spfl let abstract_tactic_expr te tacfun gls = let (sgl_sigma,v) = tacfun gls in @@ -778,9 +774,13 @@ let extract_pftreestate pts = (str"Cannot extract from a proof-tree in which we have descended;" ++ spc () ++ str"Please ascend to the root"); let pfterm,subgoals = extract_open_pftreestate pts in - if subgoals <> [] then + let exl = Evd.non_instantiated pts.tpfsigma in + if subgoals <> [] or exl <> [] then errorlabstrm "extract_proof" - (str "Attempt to save an incomplete proof"); + (if subgoals <> [] then + str "Attempt to save an incomplete proof" + else + str "Attempt to save a proof with existential variables still non-instantiated"); let env = Global.env_of_context pts.tpf.goal.evar_hyps in strong whd_betaiotaevar env pts.tpfsigma pfterm (*** diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index 60a0a937..cd8d34db 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tacexpr.ml,v 1.33.2.2 2005/01/21 17:14:09 herbelin Exp $ i*) +(*i $Id: tacexpr.ml,v 1.33.2.3 2005/05/15 12:47:04 herbelin Exp $ i*) open Names open Topconstr @@ -146,12 +146,12 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = (* Automation tactics *) | TacTrivial of string list option - | TacAuto of int option * string list option + | TacAuto of int or_var option * string list option | TacAutoTDB of int option | TacDestructHyp of (bool * identifier located) | TacDestructConcl | TacSuperAuto of (int option * reference list * bool * bool) - | TacDAuto of int option * int option + | TacDAuto of int or_var option * int option (* Context management *) | TacClear of 'id list -- cgit v1.2.3