Imported Upstream version 8.4pl2dfsgupstream/8.4pl2dfsg

11 files changed, 95 insertions, 63 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index f7d63dcd..44fea151 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -829,7 +829,8 @@ let prepare_hint env (sigma,c) =
 
 let path_of_constr_expr c =
   match c with
-  | Topconstr.CRef r -> (try PathHints [global r] with _ -> PathAny)
+  | Topconstr.CRef r ->
+    (try PathHints [global r] with e when Errors.noncritical e -> PathAny)
   | _ -> PathAny
       
 let interp_hints h =
@@ -1170,9 +1171,9 @@ let tclLOG (dbg,depth,trace) pp tac =
 	  let out = tac gl in
 	  msg_debug (str s ++ spc () ++ pp () ++ str ". (*success*)");
 	  out
-	with e ->
+	with reraise ->
 	  msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)");
-	  raise e
+	  raise reraise
       end
     | Info ->
       (* For "info (trivial/auto)", we store a log trace *)
@@ -1181,9 +1182,9 @@ let tclLOG (dbg,depth,trace) pp tac =
 	  let out = tac gl in
 	  trace := (depth, Some pp) :: !trace;
 	  out
-	with e ->
+	with reraise ->
 	  trace := (depth, None) :: !trace;
-	  raise e
+	  raise reraise
       end
 
 (** For info, from the linear trace information, we reconstitute the part
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 039f022d..8e1d7cbf 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -208,8 +208,14 @@ let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl gl =
 
 (* Functions necessary to the library object declaration *)
 let cache_hintrewrite (_,(rbase,lrl)) =
-  let base = try find_base rbase with _ -> HintDN.empty in
-  let max = try fst (Util.list_last (HintDN.find_all base)) with _ -> 0 in
+  let base =
+    try find_base rbase
+    with e when Errors.noncritical e -> HintDN.empty
+  in
+  let max =
+    try fst (Util.list_last (HintDN.find_all base))
+    with e when Errors.noncritical e -> 0
+  in
   let lrl = HintDN.map (fun (i,h) -> (i + max, h)) lrl in
     rewtab:=Stringmap.add rbase (HintDN.union lrl base) !rewtab
 
@@ -248,7 +254,7 @@ let evd_convertible env evd x y =
   try
     ignore(Unification.w_unify ~flags:Unification.elim_flags env evd Reduction.CONV x y); true 
   (* try ignore(Evarconv.the_conv_x env x y evd); true *)
-  with _ -> false
+  with e when Errors.noncritical e -> false
 
 let decompose_applied_relation metas env sigma c ctype left2right =
   let find_rel ty =
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index cf4a267f..d05ae680 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -685,7 +685,7 @@ let resolve_typeclass_evars debug m env evd filter split fail =
   let evd = 
     try Evarconv.consider_remaining_unif_problems
       ~ts:(Typeclasses.classes_transparent_state ()) env evd
-    with _ -> evd
+    with e when Errors.noncritical e -> evd
   in
     resolve_all_evars debug m env (initial_select_evars filter) evd split fail
 
@@ -776,7 +776,10 @@ END
 
 let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) dbs gl =
   try 
-    let dbs = list_map_filter (fun db -> try Some (Auto.searchtable_map db) with _ -> None) dbs in
+    let dbs = list_map_filter
+      (fun db -> try Some (Auto.searchtable_map db)
+        with e when Errors.noncritical e -> None) dbs
+    in
     let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in
       eauto ?limit:!typeclasses_depth ~only_classes ~st dbs gl
    with Not_found -> tclFAIL 0 (str" typeclasses eauto failed on: " ++ Printer.pr_goal gl) gl
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 68dd5dba..6981a733 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -205,7 +205,8 @@ module SearchProblem = struct
 (* 	    let gl = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
 (* 	      msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *)
 	      (lgls,pptac) :: aux tacl
-	  with e -> Refiner.catch_failerror e; aux tacl
+	  with e when Errors.noncritical e ->
+            Refiner.catch_failerror e; aux tacl
     in aux l
 
   (* Ordering of states is lexicographic on depth (greatest first) then
diff --git a/tactics/equality.ml b/tactics/equality.ml
index a352355b..1c5e4b2f 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -334,7 +334,8 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
 	  try
 	    rewrite_side_tac (!general_rewrite_clause cls
 				 lft2rgt occs (c,l) ~new_goals:[]) tac gl
-	  with e -> (* Try to see if there's an equality hidden *)
+	  with e when Errors.noncritical e ->
+            (* Try to see if there's an equality hidden *)
 	    let env' = push_rel_context rels env in
 	    let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *)
 	      match match_with_equality_type t' with
@@ -1156,7 +1157,7 @@ let injEq ipats (eq,_,(t,t1,t2) as u) eq_clause =
                 ]
 (* not a dep eq or no decidable type found *)
             ) else (raise Not_dep_pair)
-        ) with _ ->
+        ) with e when Errors.noncritical e ->
 	  inject_at_positions env sigma u eq_clause posns
 	    (fun _ -> intros_pattern no_move ipats)
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index f5fcb736..f6ecb47c 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -606,7 +606,7 @@ let hResolve_auto id c t gl =
       hResolve id c n t gl
     with
     | UserError _ as e -> raise e
-    | _ -> resolve_auto (n+1)
+    | e when Errors.noncritical e -> resolve_auto (n+1)
   in
   resolve_auto 1
 
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index 47e3b7ca..c6f32ce2 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -64,9 +64,12 @@ let is_non_recursive_type t = op2bool (match_with_non_recursive_type t)
 
 (* Test dependencies *)
 
+(* NB: we consider also the let-in case in the following function,
+   since they may appear in types of inductive constructors (see #2629) *)
+
 let rec has_nodep_prod_after n c =
   match kind_of_term c with
-    | Prod (_,_,b) ->
+    | Prod (_,_,b) | LetIn (_,_,_,b) ->
 	( n>0 || not (dependent (mkRel 1) b))
 	&& (has_nodep_prod_after (n-1) b)
     | _            -> true
@@ -355,7 +358,10 @@ let coq_jmeq_pattern = lazy PATTERN [ %coq_jmeq_ref ?X1 ?X2 ?X3 ?X4 ]
 let coq_eq_true_pattern = lazy PATTERN [ %coq_eq_true_ref ?X1 ]
 
 let match_eq eqn eq_pat =
-  let pat = try Lazy.force eq_pat with _ -> raise PatternMatchingFailure in
+  let pat =
+    try Lazy.force eq_pat
+    with e when Errors.noncritical e -> raise PatternMatchingFailure
+  in
   match matches pat eqn with
     | [(m1,t);(m2,x);(m3,y)] ->
 	assert (m1 = meta1 & m2 = meta2 & m3 = meta3);
diff --git a/tactics/inv.ml b/tactics/inv.ml
index b7f6addc..e4b3bdb1 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -497,7 +497,7 @@ let wrap_inv_error id = function
 (* The most general inversion tactic *)
 let inversion inv_kind status names id gls =
   try (raw_inversion inv_kind id status names) gls
-  with e -> wrap_inv_error id e
+  with e when Errors.noncritical e -> wrap_inv_error id e
 
 (* Specializing it... *)
 
@@ -540,7 +540,7 @@ let invIn k names ids id gls =
        inversion (false,k) NoDep names id;
        intros_replace_ids])
     gls
-  with e -> wrap_inv_error id e
+  with e when Errors.noncritical e -> wrap_inv_error id e
 
 let invIn_gen k names idl = try_intros_until (invIn k names idl)
 
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index b90a911a..98885af8 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -121,7 +121,7 @@ let is_applied_rewrite_relation env sigma rels t =
 	      let inst = mkApp (Lazy.force rewrite_relation_class, [| evar; mkApp (c, params) |]) in
 	      let _ = Typeclasses.resolve_one_typeclass env' evd inst in
 		Some (it_mkProd_or_LetIn t rels)
-	  with _ -> None)
+	  with e when Errors.noncritical e -> None)
   | _ -> None
 
 let _ =
@@ -145,11 +145,14 @@ let build_signature evars env m (cstrs : (types * types option) option list)
     new_cstr_evar evars env
       (* ~src:(dummy_loc, ImplicitArg (ConstRef (Lazy.force respectful), (n, Some na))) *) t
   in
-  let mk_relty evars env ty obj =
+  let mk_relty evars newenv ty obj =
     match obj with
       | None | Some (_, None) ->
 	  let relty = mk_relation ty in
-	    new_evar evars env relty
+	    if closed0 ty then 
+	      let env' = Environ.reset_with_named_context (Environ.named_context_val env) env in
+		new_evar evars env' relty
+	    else new_evar evars newenv relty
       | Some (x, Some rel) -> evars, rel
   in
   let rec aux env evars ty l =
@@ -227,7 +230,7 @@ let cstrevars evars = snd evars
 
 let evd_convertible env evd x y =
   try ignore(Evarconv.the_conv_x env x y evd); true
-  with _ -> false
+  with e when Errors.noncritical e -> false
 
 let rec decompose_app_rel env evd t = 
   match kind_of_term t with
@@ -493,7 +496,7 @@ let rec apply_pointwise rel = function
   | [] -> rel
 
 let pointwise_or_dep_relation n t car rel =
-  if noccurn 1 car then
+  if noccurn 1 car && noccurn 1 rel then
     mkApp (Lazy.force pointwise_relation, [| t; lift (-1) car; lift (-1) rel |])
   else
     mkApp (Lazy.force forall_relation, 
@@ -1048,7 +1051,8 @@ module Strategies =
 	let sigma, c = Constrintern.interp_open_constr (goalevars evars) env c in
 	let unfolded =
 	  try Tacred.try_red_product env sigma c
-	  with _ -> error "fold: the term is not unfoldable !"
+	  with e when Errors.noncritical e ->
+            error "fold: the term is not unfoldable !"
 	in
 	  try
 	    let sigma = Unification.w_unify env sigma CONV ~flags:Unification.elim_flags unfolded t in
@@ -1056,7 +1060,7 @@ module Strategies =
 	      Some (Some { rew_car = ty; rew_from = t; rew_to = c';
 			   rew_prf = RewCast DEFAULTcast; 
 			   rew_evars = sigma, cstrevars evars })
-	  with _ -> None
+	  with e when Errors.noncritical e -> None
 
     let fold_glob c : strategy =
       fun env avoid t ty cstr evars ->
@@ -1064,7 +1068,8 @@ module Strategies =
 	let sigma, c = Pretyping.Default.understand_tcc (goalevars evars) env c in
 	let unfolded =
 	  try Tacred.try_red_product env sigma c
-	  with _ -> error "fold: the term is not unfoldable !"
+	  with e when Errors.noncritical e ->
+            error "fold: the term is not unfoldable !"
 	in
 	  try
 	    let sigma = Unification.w_unify env sigma CONV ~flags:Unification.elim_flags unfolded t in
@@ -1072,7 +1077,7 @@ module Strategies =
 	      Some (Some { rew_car = ty; rew_from = t; rew_to = c';
 			   rew_prf = RewCast DEFAULTcast; 
 			   rew_evars = sigma, cstrevars evars })
-	  with _ -> None
+	  with e when Errors.noncritical e -> None
   
 
 end
@@ -1977,7 +1982,7 @@ let setoid_proof gl ty fn fallback =
       let evm = project gl in
       let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env evm rel)))) in
 	fn env evm car rel gl
-    with e ->
+    with e when Errors.noncritical e ->
       try fallback gl
       with Hipattern.NoEquationFound ->
 	  match e with
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 3ff0cf93..7479ee9a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -50,7 +50,7 @@ open Compat
 open Evd
 
 let safe_msgnl s =
-    try msgnl s with e ->
+    try msgnl s with e when Errors.noncritical e ->
       msgnl
 	(str "bug in the debugger: " ++
          str "an exception is raised while printing debug information")
@@ -92,7 +92,7 @@ let catch_error call_trace tac g =
   if call_trace = [] then tac g else try tac g with
   | LtacLocated _ as e -> raise e
   | Loc.Exc_located (_,LtacLocated _) as e -> raise e
-  | e ->
+  | e when Errors.noncritical e ->
     let (nrep,loc',c),tail = list_sep_last call_trace in
     let loc,e' = match e with Loc.Exc_located(loc,e) -> loc,e | _ ->dloc,e in
     if tail = [] then
@@ -569,13 +569,13 @@ let dump_glob_red_expr = function
     try
       Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r)
 	(Smartlocate.smart_global r)
-    with _ -> ()) occs
+    with e when Errors.noncritical e -> ()) occs
   | Cbv grf | Lazy grf ->
     List.iter (fun r ->
       try
         Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r)
 	  (Smartlocate.smart_global r)
-      with _ -> ()) grf.rConst
+      with e when Errors.noncritical e -> ()) grf.rConst
   | _ -> ()
 
 let intern_red_expr ist = function
@@ -1412,19 +1412,20 @@ let interp_may_eval f ist gl = function
   | ConstrTerm c ->
      try
 	f ist gl c
-     with e ->
-       debugging_exception_step ist false e (fun () ->
+     with reraise ->
+       debugging_exception_step ist false reraise (fun () ->
          str"interpretation of term " ++ pr_glob_constr_env (pf_env gl) (fst c));
-       raise e
+       raise reraise
 
 (* Interprets a constr expression possibly to first evaluate *)
 let interp_constr_may_eval ist gl c =
   let (sigma,csr) =
     try
       interp_may_eval pf_interp_constr ist gl c
-    with e ->
-      debugging_exception_step ist false e (fun () -> str"evaluation of term");
-      raise e
+    with reraise ->
+      debugging_exception_step ist false reraise (fun () ->
+        str"evaluation of term");
+      raise reraise
   in
   begin
     db_constr ist.debug (pf_env gl) csr;
@@ -1762,10 +1763,7 @@ let mk_int_or_var_value ist c = VInteger (interp_int_or_var ist c)
 let pack_sigma (sigma,c) = {it=c;sigma=sigma}
 
 let extend_gl_hyps { it=gl ; sigma=sigma } sign =
-  let hyps = Goal.V82.hyps sigma gl in
-  let new_hyps = List.fold_right Environ.push_named_context_val sign hyps in
-  (* spiwack: (2010/01/13) if a bug was reintroduced in [change] in is probably here *)
-  Goal.V82.new_goal_with sigma gl new_hyps
+  Goal.V82.new_goal_with sigma gl sign
 
 (* Interprets an l-tac expression into a value *)
 let rec val_interp ist gl (tac:glob_tactic_expr) =
@@ -1925,9 +1923,11 @@ and interp_app loc ist gl fv largs =
 	    try
 	      catch_error trace
 		(val_interp {ist with lfun=newlfun@olfun; trace=trace} gl) body
-	    with e ->
-              debugging_exception_step ist false e (fun () -> str "evaluation");
-	      raise e in
+	    with reraise ->
+              debugging_exception_step ist false reraise
+                (fun () -> str "evaluation");
+	      raise reraise
+          in
 	  let gl = { gl with sigma=sigma } in
           debugging_step ist
 	    (fun () ->
@@ -2212,19 +2212,20 @@ and interp_match ist g lz constr lmr =
         (try
             let lmatch =
               try extended_matches c csr
-              with e ->
-                debugging_exception_step ist false e (fun () ->
+              with reraise ->
+                debugging_exception_step ist false reraise (fun () ->
                   str "matching with pattern" ++ fnl () ++
                   pr_constr_pattern_env (pf_env g) c);
-                raise e in
+                raise reraise
+            in
             try
               let lfun = extend_values_with_bindings lmatch ist.lfun in
               eval_with_fail { ist with lfun=lfun } lz g mt
-            with e ->
-              debugging_exception_step ist false e (fun () ->
+            with reraise ->
+              debugging_exception_step ist false reraise (fun () ->
                 str "rule body for pattern" ++
                 pr_constr_pattern_env (pf_env g) c);
-              raise e
+              raise reraise
          with e when is_match_catchable e ->
            debugging_step ist (fun () -> str "switching to the next rule");
            apply_match ist sigma csr tl)
@@ -2236,15 +2237,16 @@ and interp_match ist g lz constr lmr =
       errorlabstrm "Tacinterp.apply_match" (str
         "No matching clauses for match.") in
   let (sigma,csr) =
-      try interp_ltac_constr ist g constr with e ->
-        debugging_exception_step ist true e
+      try interp_ltac_constr ist g constr with reraise ->
+        debugging_exception_step ist true reraise
           (fun () -> str "evaluation of the matched expression");
-        raise e in
+        raise reraise in
   let ilr = read_match_rule (fst (extract_ltac_constr_values ist (pf_env g))) ist (pf_env g) sigma lmr in
   let res =
-     try apply_match ist sigma csr ilr with e ->
-       debugging_exception_step ist true e (fun () -> str "match expression");
-       raise e in
+     try apply_match ist sigma csr ilr with reraise ->
+       debugging_exception_step ist true reraise
+         (fun () -> str "match expression");
+       raise reraise in
   debugging_step ist (fun () ->
     str "match expression returns " ++ pr_value (Some (pf_env g)) (snd res));
   res
@@ -2404,6 +2406,7 @@ and interp_atomic ist gl tac =
 	(h_generalize_dep c_interp)
   | TacLetTac (na,c,clp,b,eqpat) ->
       let clp = interp_clause ist gl clp in
+      let eqpat = Option.map (interp_intro_pattern ist gl) eqpat in
       if clp = nowhere then
         (* We try to fully-typecheck the term *)
 	let (sigma,c_interp) = pf_interp_constr ist gl c in
@@ -3180,7 +3183,8 @@ let globTacticIn t = TacArg (dloc,TacDynamic (dloc,tactic_in t))
 let tacticIn t =
   globTacticIn (fun ist ->
     try glob_tactic (t ist)
-    with e -> anomalylabstrm "tacticIn"
+    with e when Errors.noncritical e ->
+      anomalylabstrm "tacticIn"
       (str "Incorrect tactic expression. Received exception is:" ++
        Errors.print e))
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 12292196..ac00a73d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1018,7 +1018,7 @@ let apply_in_once_main flags innerclause (d,lbind) gl =
   let thm = nf_betaiota gl.sigma (pf_type_of gl d) in
   let rec aux clause =
     try progress_with_clause flags innerclause clause
-    with err ->
+    with err when Errors.noncritical err ->
     try aux (clenv_push_prod clause)
     with NotExtensibleClause -> raise err in
   aux (make_clenv_binding gl (d,thm) lbind)
@@ -1708,7 +1708,7 @@ let make_pattern_test env sigma0 (sigma,c) =
   let flags = default_matching_flags sigma0 in
   let matching_fun t =
     try let sigma = w_unify env sigma Reduction.CONV ~flags c t in Some(sigma,t)
-    with _ -> raise NotUnifiable in
+    with e when Errors.noncritical e -> raise NotUnifiable in
   let merge_fun c1 c2 =
     match c1, c2 with
     | Some (_,c1), Some (_,c2) when not (is_fconv Reduction.CONV env sigma0 c1 c2) ->
@@ -2554,7 +2554,10 @@ let specialize_eqs id gl =
       
 
 let specialize_eqs id gl =
-  if try ignore(clear [id] gl); false with _ -> true then
+  if
+    (try ignore(clear [id] gl); false
+     with e when Errors.noncritical e -> true)
+  then
     tclFAIL 0 (str "Specialization not allowed on dependent hypotheses") gl 
   else specialize_eqs id gl
 
@@ -2716,7 +2719,8 @@ let compute_elim_sig ?elimc elimt =
       | Some ( _,None,ind) ->
 	  let indhd,indargs = decompose_app ind in
 	  try {!res with indref = Some (global_of_constr indhd) }
-	  with _ -> error "Cannot find the inductive type of the inductive scheme.";;
+	  with e when Errors.noncritical e ->
+            error "Cannot find the inductive type of the inductive scheme.";;
 
 let compute_scheme_signature scheme names_info ind_type_guess =
   let f,l = decompose_app scheme.concl in
@@ -3551,4 +3555,5 @@ let unify ?(state=full_transparent_state) x y gl =
     in
     let evd = w_unify (pf_env gl) (project gl) Reduction.CONV ~flags x y
     in tclEVARS evd gl
-  with _ -> tclFAIL 0 (str"Not unifiable") gl
+  with e when Errors.noncritical e ->
+    tclFAIL 0 (str"Not unifiable") gl