Imported Upstream version 8.4pl2dfsgupstream/8.4pl2dfsg

1 files changed, 15 insertions, 10 deletions

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