Attempt to capture on time unification errors for "with" bindings.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12450 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 22 insertions, 7 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index d21c8ad45a..9ce46ab8a3 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -404,8 +404,10 @@ let clenv_unify_binding_type clenv c t u =
     try
       let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in
       TypeProcessed, { clenv with evd = evd }, c
-    with e when precatchable_exception e ->
-      TypeNotProcessed, clenv, c
+    with 
+      | PretypeError (_,NotClean _) as e -> raise e
+      | e when precatchable_exception e ->
+	  TypeNotProcessed, clenv, c
 
 let clenv_assign_binding clenv k (sigma,c) =
   let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 3d3b3b9ef3..6423ad14e8 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -213,10 +213,11 @@ Goal True.
 set (p:=fun j => j (or_intror _ (fun a:True => j (or_introl _ a)))) || idtac.
 Abort.
 
-(* remark: the following example does not succeed any longer in 8.2 because,
-   the algorithm is more general and does exclude a solution that it should
-   exclude for typing reason. Handling of types and backtracking is still to
-   be done
+(* Remark: the following example stopped succeeding at some time in
+   the development of 8.2 but it works again (this was because 8.2
+   algorithm was more general and did not exclude a solution that it
+   should have excluded for typing reason; handling of types and
+   backtracking is still to be done) *)
 
 Section S.
 Variables A B : nat -> Prop.
@@ -224,4 +225,16 @@ Goal forall x : nat, A x -> B x.
 refine (fun x H => proj2 (_ x H) _).
 Abort.
 End S.
-*)
+
+(* Check that constraints are taken into account by tactics that instantiate *)
+
+Lemma inj : forall n m, S n = S m -> n = m.
+intros n m H.
+eapply f_equal with (* should fail because ill-typed *)
+  (f := fun n =>
+        match n return match n with S _ => nat | _ => unit end with
+        | S n => n
+        | _ => tt
+        end) in H
+|| injection H.
+Abort.