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, 7 insertions, 7 deletions

diff --git a/Makefile b/Makefile
index 2de542be20..88beb3d509 100644
--- a/Makefile
+++ b/Makefile
@@ -155,9 +155,9 @@ PRETYPING=\
   pretyping/reductionops.cmo pretyping/vnorm.cmo pretyping/inductiveops.cmo \
   pretyping/retyping.cmo pretyping/cbv.cmo \
   pretyping/pretype_errors.cmo pretyping/recordops.cmo pretyping/typing.cmo \
-  pretyping/tacred.cmo \
-  pretyping/evarutil.cmo pretyping/unification.cmo pretyping/evarconv.cmo \
-  pretyping/classops.cmo pretyping/coercion.cmo pretyping/clenv.cmo \
+  pretyping/tacred.cmo pretyping/evarutil.cmo pretyping/evarconv.cmo \
+  pretyping/classops.cmo pretyping/coercion.cmo \
+  pretyping/unification.cmo pretyping/clenv.cmo \
   pretyping/rawterm.cmo pretyping/pattern.cmo \
   pretyping/detyping.cmo  pretyping/indrec.cmo\
   pretyping/cases.cmo pretyping/pretyping.cmo pretyping/matching.cmo
@@ -1497,14 +1497,14 @@ PRINTERSCMO=\
   library/summary.cmo library/global.cmo library/nameops.cmo		\
   library/libnames.cmo library/nametab.cmo library/libobject.cmo	\
   library/lib.cmo library/goptions.cmo \
-  pretyping/termops.cmo pretyping/evd.cmo				    \
-  pretyping/rawterm.cmo pretyping/termops.cmo pretyping/evd.cmo		    \
+  pretyping/termops.cmo pretyping/evd.cmo pretyping/rawterm.cmo \
   pretyping/reductionops.cmo pretyping/inductiveops.cmo			    \
   pretyping/retyping.cmo pretyping/cbv.cmo				    \
   pretyping/pretype_errors.cmo pretyping/recordops.cmo pretyping/typing.cmo \
-  pretyping/evarutil.cmo pretyping/unification.cmo pretyping/evarconv.cmo   \
+  pretyping/evarutil.cmo pretyping/evarconv.cmo   \
   pretyping/tacred.cmo pretyping/classops.cmo pretyping/detyping.cmo	    \
-  pretyping/indrec.cmo pretyping/coercion.cmo pretyping/cases.cmo	    \
+  pretyping/indrec.cmo pretyping/coercion.cmo \
+  pretyping/unification.cmo pretyping/cases.cmo \
   pretyping/pretyping.cmo pretyping/clenv.cmo pretyping/pattern.cmo \
   parsing/lexer.cmo interp/ppextend.cmo interp/genarg.cmo \
   interp/topconstr.cmo interp/notation.cmo interp/reserve.cmo		\