Imported Upstream version 8.0pl3upstream/8.0pl3

3 files changed, 23 insertions, 25 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)
 
 
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