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

diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 6b0f8413a..0c2024162 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -30,6 +30,7 @@ open Rawterm
 
 val inj_open : constr -> open_constr
 val inj_red_expr : red_expr -> (open_constr, evaluable_global_reference) red_expr_gen
+val inj_ebindings : constr bindings -> open_constr bindings
 
 (* Main tactics. *)
 
@@ -169,9 +170,11 @@ val bring_hyps : named_context -> tactic
 val apply                 : constr      -> tactic
 val apply_without_reduce  : constr      -> tactic
 val apply_list            : constr list -> tactic
-val apply_with_bindings_gen   : evars_flag -> constr with_ebindings -> tactic
-val apply_with_bindings : constr with_ebindings -> tactic
-val eapply_with_bindings  : constr with_ebindings -> tactic
+val apply_with_ebindings_gen : evars_flag -> constr with_ebindings -> tactic
+val apply_with_bindings   : constr with_bindings -> tactic
+val apply_with_ebindings  : constr with_ebindings -> tactic
+val eapply_with_bindings  : constr with_bindings -> tactic
+val eapply_with_ebindings : constr with_ebindings -> tactic
 
 val cut_and_apply         : constr -> tactic
 
@@ -271,11 +274,17 @@ val constructor_tac            : int option -> int ->
                                  open_constr bindings  -> tactic
 val one_constructor            : int -> open_constr bindings  -> tactic
 val any_constructor            : tactic option -> tactic
-val left                       : open_constr bindings -> tactic
+
+val left                       : constr bindings -> tactic
+val right                      : constr bindings -> tactic
+val split                      : constr bindings -> tactic
+
+val left_with_ebindings        : open_constr bindings -> tactic
+val right_with_ebindings       : open_constr bindings -> tactic
+val split_with_ebindings       : open_constr bindings -> tactic
+
 val simplest_left              : tactic
-val right                      : open_constr bindings -> tactic
 val simplest_right             : tactic
-val split                      : open_constr bindings -> tactic
 val simplest_split             : tactic
 
 (*s Logical connective tactics. *)