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

diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index 49791c367..5f45d9d85 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
+(* $Id:$ *)
+
 open Term
 open Termops
 open Environ
@@ -416,8 +418,8 @@ let base_leaf_terminate (func:global_reference) eqs expr =
 	   [k';h] -> k',h
 	 | _ -> assert false
      in
-     tclTHENLIST [observe_tac "first split" (split (ImplicitBindings [inj_open expr]));
-		  observe_tac "second split" (split (ImplicitBindings [inj_open (delayed_force coq_O)]));
+     tclTHENLIST [observe_tac "first split" (split (ImplicitBindings [expr]));
+		  observe_tac "second split" (split (ImplicitBindings [delayed_force coq_O]));
 		  observe_tac "intro k" (h_intro k');
                   observe_tac "case on k" 
 		      (tclTHENS 
@@ -459,7 +461,7 @@ let rec compute_le_proofs = function
 	      in
 	      apply_with_bindings
 		(le_trans,
-		 ExplicitBindings[dummy_loc,NamedHyp m_id,inj_open a])
+		 ExplicitBindings[dummy_loc,NamedHyp m_id,a])
 		g
 	   )
 	   [compute_le_proofs tl; 
@@ -477,7 +479,7 @@ let make_lt_proof pmax le_proof =
        in
        apply_with_bindings
 	 (le_lt_trans,
-	  ExplicitBindings[dummy_loc,NamedHyp m_id, inj_open pmax]) g)
+	  ExplicitBindings[dummy_loc,NamedHyp m_id, pmax]) g)
     [observe_tac "compute_le_proofs" (compute_le_proofs le_proof); 
      tclTHENLIST[observe_tac "lt_S_n" (apply (delayed_force lt_S_n)); default_full_auto]];;
 
@@ -496,8 +498,8 @@ let rec list_cond_rewrite k def pmax cond_eqs le_proofs =
 	 tclTHENS
 	   (general_rewrite_bindings false
 	      (mkVar eq,
-	       ExplicitBindings[dummy_loc, NamedHyp k_id, inj_open (mkVar k);
-				dummy_loc, NamedHyp def_id, inj_open (mkVar def)]) false)
+	       ExplicitBindings[dummy_loc, NamedHyp k_id, mkVar k;
+				dummy_loc, NamedHyp def_id, mkVar def]) false)
 	   [list_cond_rewrite k def pmax eqs le_proofs;
             observe_tac "make_lt_proof" (make_lt_proof pmax le_proofs)] g
       ) 
@@ -515,7 +517,7 @@ let rec introduce_all_equalities func eqs values specs bound le_proofs
         let ids = h'::ids in
 	let def = next_global_ident_away true def_id ids in
 	tclTHENLIST
-	  [observe_tac "introduce_all_equalities_final split" (split (ImplicitBindings [inj_open s_max]));
+	  [observe_tac "introduce_all_equalities_final split" (split (ImplicitBindings [s_max]));
 	   observe_tac "introduce_all_equalities_final intro k" (h_intro  k);
 	   tclTHENS
 	     (observe_tac "introduce_all_equalities_final case k" (simplest_case (mkVar k)))
@@ -575,8 +577,8 @@ let rec introduce_all_values is_mes acc_inv func context_fn
     (match args with
     [] -> 
       tclTHENLIST
-	[observe_tac "split" (split(ImplicitBindings 
-		 [inj_open (context_fn (List.map mkVar (List.rev values)))]));
+	[observe_tac "split" (split(ImplicitBindings
+		 [context_fn (List.map mkVar (List.rev values))]));
 	 observe_tac "introduce_all_equalities" (introduce_all_equalities func eqs
 	   (List.rev values) (List.rev specs) (delayed_force coq_O) [] [])]
   | arg::args ->
@@ -1194,9 +1196,9 @@ let rec introduce_all_values_eq  cont_tac functional termine
 		general_rewrite_bindings false
 		(mkVar heq1,
 		 ExplicitBindings[dummy_loc,NamedHyp k_id,
-		                  inj_open (f_S(f_S(mkVar pmax)));
+				  f_S(f_S(mkVar pmax));
 				  dummy_loc,NamedHyp def_id,
-				  inj_open f]) false gls )
+				  f]) false gls )
 	     [tclTHENLIST
 		[simpl_iter();
 		 unfold_constr (reference_of_constr functional);
@@ -1247,8 +1249,8 @@ let rec introduce_all_values_eq  cont_tac functional termine
 			   (mkVar heq,
 			    ExplicitBindings
 			      [dummy_loc, NamedHyp k_id,
-			       inj_open (f_S(mkVar pmax'));
-			       dummy_loc, NamedHyp def_id, inj_open f]) false))
+			       f_S(mkVar pmax');
+			       dummy_loc, NamedHyp def_id, f]) false))
 			   g
 		     )
 		     [tclIDTAC;