Raffinement de l'algorithme d'inférence de type

-----------------------------------------------

- Les fonctions evar_define et real_clean font un travail plus fin :
  - S'il y a plusieurs manières d'inverser l'instance d'une evar, on
    retarde le choix au lieu de faire un choix arbitraire.
  - Si l'instance contient une evar et que cette evar n'est pas inversible,
    on essaie aussi d'inverser ou de restreindre (un sous-terme) de 
    l'evar qui était initialement à instancier.
  - Incidemment, real_clean est renommé en invert_instance, un nom qui
    reflète mieux la diversité du travail fait par ce fameux real_clean.
- La fonction solve_refl garde les problèmes qui contiennent encore de
  l'information.
- Changements secondaires :
  - Délégation de la gestion des variables modifiées et des problèmes à
    reconsidérer (get_conv_pbs) à Evd (qui s'en charge par effet de bord
    au moment du define) (incidemment get_conv_pbs devient
    extract_conv_pbs)
  - Essai d'un mécanisme différent de restriction des evars : pour
    éviter des contextes mal formés (comme do_restrict pouvait a priori
    le faire), on utilise maintenant un contexte bien formé doublé d'un
    filtre signalant les instances interdites. C'est a priori plus
    souple (par ex : si une variable du contexte a un type dépendant
    d'une evar, on peut attendre de connaître cette evar avec de
    déterminer si cette variable du contexte, qui peut-être dépend via
    cette evar d'une autre variable interdite, doit être finalement
    interdite ou pas)
  - Nettoyages divers.
- Ce que evarutil ne fait toujours pas :
  - Utiliser l'inversion et/ou l'unification d'ordre supérieur (par
    exemple pour résoudre "?ev[S n]=n"); en particulier, la notion
    d'inversion unique ne prend pas en compte l'unification d'ordre
    supérieur et peut donc faire des choix irréversibles vis à vis de
    l'unif d'ordre supérieur.
  - Utiliser (systématiquement -- et précautionneusement) les types
    des solutions trouvées pour résoudre davantage de problèmes.



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

2 files changed, 4 insertions, 11 deletions

diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index 415f533a69..649db86ce9 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -176,13 +176,9 @@ let ltac_lcall tac args =
 
 let carg c = TacDynamic(dummy_loc,Pretyping.constr_in c)
 
-let dummy_goal env =
-  {Evd.it=
-    {Evd.evar_concl=mkProp;
-     Evd.evar_hyps=named_context_val env;
-     Evd.evar_body=Evd.Evar_empty;
-     Evd.evar_extra=None};
-   Evd.sigma=Evd.empty}
+let dummy_goal env = 
+  {Evd.it = Evd.make_evar (named_context_val env) mkProp;
+   Evd.sigma = Evd.empty}
 
 let exec_tactic env n f args =
   let lid = list_tabulate(fun i -> id_of_string("x"^string_of_int i)) n in
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 656c4397d3..76f79443e1 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -51,10 +51,7 @@ let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Obj.magic ())
 
 let set_default_tactic t = default_tactic_expr := t; default_tactic := Tacinterp.eval_tactic t
 
-let evar_of_obligation o = { evar_hyps = Global.named_context_val () ;
-			     evar_concl = o.obl_type ; 
-			     evar_body = Evar_empty ;
-			     evar_extra = None }
+let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type
 
 let subst_deps obls deps t =
   Intset.fold