Unification suite: petits affinements pour préserver la compatibilité

(en particulier, la décision de quelle instance garder quand une méta
a plusieurs solutions importe; comment trouver une critère objectif ?
la compatibilité demande à donner préférence aux instances trouvées
par with-bindings).



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

3 files changed, 28 insertions, 8 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index a08c626256..edf9056419 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 bd6fb5ad88..372188e8a0 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 fb6250d509..adb55cf2c5 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.