diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-01-19 22:34:29 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-01-19 22:34:29 +0000 |
| commit | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (patch) | |
| tree | fbb91e2f74c73bb867ab62c58f248a704bbe6dec /proofs/logic.ml | |
| parent | 6497f27021fec4e01f2182014f2bb1989b4707f9 (diff) | |
Imported Upstream version 8.0pl3upstream/8.0pl3
Diffstat (limited to 'proofs/logic.ml')
| -rw-r--r-- | proofs/logic.ml | 26 |
1 files changed, 12 insertions, 14 deletions
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) |