Nouvelle stratégie d'unification des types des with-bindings dans

apply afin de reculer au plus tard les décisions irréversibles et en
particulier de pouvoir typer les with-bindings modulo coercions :

  - l'unification des types des métas données en with-bindings est
    retardé à après l'unification (unify_0) de telle sorte que les
    instances trouvées par unify_0 soient prioritaires et que la
    décision d'insérer éventuellement des coercions autour des valeurs
    données en with-bindings se fasse au dernier moment;
  - toujours pour permettre d'insérer ultimement des coercions, 
    l'instantiation des with-bindings ne se fait plus
    l'appel unify_0 (cf clenv_unique_resolver);
  - pour permettre ce retardement sans limiter le test de conversion
    que unify_0 fait sur les termes clos, on transmet à unify_0 les
    métas données en with-bindings (ainsi l'instantiation de ces métas
    peut être faite dynamiquement au moment du test de clôture);
  - parce que les métas données en with-bindings qui sont en position
    de rédex (cas d'un "apply f_equal with (f:=fun ...)" peuvent
    simplifier le problème d'unification (et elles ne sont pas de
    toutes façons pas réinférables au premier ordre), on continue à
    les substituer avant l'appel à unify_0 (cf meta_reducible_instance);
  - pour l'unification du second-ordre, on continue d'instancier les
    with-bindings et d'unifier les types des with-bindings avant
    unification;
  - reste à régler un problème de compatibilité lorsque le résultat de
    l'unification des types des with-bindings est utilisé pour rendre
    un terme clos et pour permettre à unify_0 d'utiliser la conversion.

+ meilleure compatibilité de apply, split, left, right pour le code
  qui l'utilise avec des bindings clos
+ nettoyage et uniformisation des clenv_match_args, clenv_missing, et assimilés



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

1 files changed, 65 insertions, 0 deletions

diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 3c9fbeb364..fb6250d509 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -28,3 +28,68 @@ Notation S':=S (only parsing).
 Goal (forall S, S = S' S) -> (forall S, S = S' S).
 intros.
 apply H with (S0 := S).
+
+(* Check inference of implicit arguments in bindings *)
+
+Goal exists y : nat -> Type, y 0 = y 0.
+exists (fun x => True).
+trivial.
+Qed.
+
+(* Check universe handling in typed unificationn *)
+
+Definition E := Type.
+Goal exists y : E, y = y.
+exists Prop.
+trivial.
+Qed.
+
+Definition E := Type.
+Variable Eq : Prop = (Prop -> Prop) :> E.
+Goal Prop.
+rewrite Eq.
+Abort.
+
+(* Check insertion of coercions in bindings *)
+
+Coercion eq_true : bool >-> Sortclass.
+Goal exists A:Prop, A = A.
+exists true.
+trivial.
+Qed.
+
+(* Check use of unification of bindings types in specialize *)
+
+Variable P : nat -> Prop.
+Variable L : forall (l : nat), P l -> P l.
+Goal P 0 -> True.
+intros.
+specialize L with (1:=H).
+Abort.
+Reset P.
+
+(* Two examples that show that hnf_constr is used when unifying types
+   of bindings *)
+
+Require Import List.
+Open Scope list_scope.
+Fixpoint P (l : list nat) : Prop :=
+  match l with
+  | nil => True
+  | e1 :: nil => e1 = e1
+  | e1 :: l1 => e1 = e1 /\ P l1
+  end.
+Variable L : forall n l, P (n::l) -> P l.
+
+Goal forall (x:nat) l, P (x::l) -> P l.
+intros.
+apply L with (1:=H).
+Qed.
+
+Goal forall (x:nat) l, match l with nil => x=x | _::_ => x=x /\ P l end -> P l.
+intros.
+apply L with (1:=H).
+Qed.
+
+
+