diff options
| -rw-r--r-- | pretyping/clenv.ml | 3 | ||||
| -rw-r--r-- | pretyping/unification.ml | 6 | ||||
| -rw-r--r-- | test-suite/success/apply.v | 27 |
3 files changed, 28 insertions, 8 deletions
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index a08c62625..edf905641 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -409,7 +409,8 @@ let clenv_unify_similar_types clenv c t u = let clenv_assign_binding clenv k (sigma,c) = let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in - let c_typ = clenv_hnf_constr clenv' (clenv_get_type_of clenv' c) in + let c_typ = nf_betaiota (clenv_get_type_of clenv' c) in + let c_typ = clenv_hnf_constr clenv' c_typ in let status,clenv'',c = clenv_unify_similar_types clenv' c c_typ k_typ in (* let evd,c' = w_coerce (cl_env clenv') c c_typ k_typ clenv'.evd in*) { clenv'' with evd = meta_assign k (c,status) clenv''.evd } diff --git a/pretyping/unification.ml b/pretyping/unification.ml index bd6fb5ad8..372188e8a 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -183,9 +183,9 @@ let unify_0_with_initial_metas metas env sigma cv_pb mod_delta m n = (if mod_delta then is_fconv (conv_pb_of cv_pb) env sigma m n else eq_constr m n) then - (metas,[]) + ([],[]) else - let (mc,ec) = unirec_rec env cv_pb (metas,[]) m n in + let (mc,ec) = unirec_rec env cv_pb ([],[]) m n in ((*sort_eqns*) mc, (*sort_eqns*) ec) let unify_0 = unify_0_with_initial_metas [] @@ -442,7 +442,7 @@ let w_unify_core_0 env with_types cv_pb mod_delta m n evd = let (mc1,evd') = retract_coercible_metas evd in let (mc2,ec) = unify_0_with_initial_metas mc1 env (evars_of evd') cv_pb mod_delta m n in - w_merge env with_types mod_delta mc2 ec evd' + w_merge env with_types mod_delta (mc1@mc2) ec evd' let w_unify_0 env = w_unify_core_0 env false let w_typed_unify env = w_unify_core_0 env true diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index fb6250d50..adb55cf2c 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -7,8 +7,7 @@ assumption. Qed. Require Import ZArith. -Open Scope Z_scope. -Goal forall x y z, ~ z <= 0 -> x * z < y * z -> x <= y. +Goal (forall x y z, ~ z <= 0 -> x * z < y * z -> x <= y)%Z. intros; apply Znot_le_gt, Zgt_lt in H. apply Zmult_lt_reg_r, Zlt_le_weak in H0; auto. Qed. @@ -28,6 +27,7 @@ Notation S':=S (only parsing). Goal (forall S, S = S' S) -> (forall S, S = S' S). intros. apply H with (S0 := S). +Qed. (* Check inference of implicit arguments in bindings *) @@ -44,7 +44,6 @@ exists Prop. trivial. Qed. -Definition E := Type. Variable Eq : Prop = (Prop -> Prop) :> E. Goal Prop. rewrite Eq. @@ -69,7 +68,7 @@ Abort. Reset P. (* Two examples that show that hnf_constr is used when unifying types - of bindings *) + of bindings (a simplification of a script from Field_Theory) *) Require Import List. Open Scope list_scope. @@ -91,5 +90,25 @@ intros. apply L with (1:=H). Qed. +(* The following call to auto fails if the type of the clause + associated to the H is not beta-reduced [but apply H works] + (a simplification of a script from FSetAVL) *) + +Definition apply (f:nat->Prop) := forall x, f x. +Goal apply (fun n => n=0) -> 1=0. +intro H. +auto. +Qed. +(* The following fails if the coercion Zpos is not introduced around p + before trying a subterm that matches the left-hand-side of the equality + (a simplication of an example taken from Nijmegen/QArith) *) +Require Import ZArith. +Coercion Zpos : positive >-> Z. +Variable f : Z -> Z -> Z. +Variable g : forall q1 q2 p : Z, f (f q1 p) (f q2 p) = Z0. +Goal forall p q1 q2, f (f q1 (Zpos p)) (f q2 (Zpos p)) = Z0. +intros; rewrite g with (p:=p). +reflexivity. +Qed. |