diff options
| -rw-r--r-- | pretyping/clenv.ml | 6 | ||||
| -rw-r--r-- | test-suite/success/evars.v | 23 |
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. |