From 7ce2a046e9a9bee93fd5f63d3938ceedb85f19f2 Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 17 Sep 2007 18:40:21 +0000 Subject: 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 --- contrib/setoid_ring/newring.ml4 | 10 +++------- contrib/subtac/subtac_obligations.ml | 5 +---- 2 files changed, 4 insertions(+), 11 deletions(-) (limited to 'contrib') 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 -- cgit v1.2.3