- Propagation des evars non résolues vers les with_bindings; permet par exemple

  de résoudre des buts comme celui-ci :

  Record nat_retract : Type := 
    {f1 : nat -> nat; f2 : nat -> nat; f1_o_f2 : forall x, f1 (f2 x) = x}.
  Goal nat_retract.
  exists (fun x => x) (fun x => x).

- Nouvelle tentative d'utilisation des types des metas/evars pour
  inférer de nouvelles instances de metas/evars; permet par exemple
  d'utiliser f_equal sans option with, mais aussi, avec la modif
  précédente, de résoudre des buts tels que

  Goal exists f:bool->Prop, f true = True.
  exists (fun x => True).

  [Les expériences passées avaient montré qu'en prenant en compte les
  types dans l'unification, on peut unifier trop tôt une evars à une
  mauvaise sorte; à défaut de mécanisme de prise en compte des problème
  d'unification avec sous-typage, on s'est interdit ici d'unifier des
  types qui sont des arités.]

- Tout les constr de tactic_expr deviennent des open_constr (même si seul
  with_bindings les accepte au final... c'est pas l'idéal).
- Renommage env -> evd et templenv -> env dans clausenv.
- Renommage closed_generic_argument -> typed_generic_argument.
- Renommage closed_abstract_argument_type -> typed_abstract_argument_type.



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

1 files changed, 4 insertions, 4 deletions

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 170f2948d4..8fc95b4086 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1734,14 +1734,14 @@ let unification_rewrite c1 c2 cl but gl =
       (* ~mod_delta:false to allow to mark occurences that must not be
          rewritten simply by replacing them with let-defined definitions
          in the context *)
-      w_unify_to_subterm ~mod_delta:false (pf_env gl) (c1,but) cl.env
+      w_unify_to_subterm ~mod_delta:false (pf_env gl) (c1,but) cl.evd
     with
 	Pretype_errors.PretypeError _ ->
 	  (* ~mod_delta:true to make Ring work (since it really
              exploits conversion) *)
-	  w_unify_to_subterm ~mod_delta:true (pf_env gl) (c1,but) cl.env
+	  w_unify_to_subterm ~mod_delta:true (pf_env gl) (c1,but) cl.evd
   in
-  let cl' = {cl with env = env' } in
+  let cl' = {cl with evd = env' } in
   let c2 = Clenv.clenv_nf_meta cl' c2 in
   check_evar_map_of_evars_defs env' ;
   env',Clenv.clenv_value cl', c1, c2
@@ -1983,7 +1983,7 @@ let setoid_transitivity c gl =
              | _ -> assert false
            in
             apply_with_bindings
-             (trans, Rawterm.ExplicitBindings [ dummy_loc, binder, c ]) gl
+             (trans, Rawterm.ExplicitBindings [ dummy_loc, binder, (Evd.empty,c) ]) gl
  with
   Optimize -> transitivity c gl
 ;;