Imported Upstream version 8.4pl2dfsgupstream/8.4pl2dfsg

9 files changed, 36 insertions, 28 deletions

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 =