diff options
author | 2009-02-19 19:13:50 +0000 | |
---|---|---|
committer | 2009-02-19 19:13:50 +0000 | |
commit | e653b53692e2cc0bb4f84881b32d3242ea39be86 (patch) | |
tree | 728e2a206876bf932c033a781e0552620f7f89d0 /interp | |
parent | a6abd9f72319cacb17e825b1f09255974c2e59f0 (diff) |
On remplace evar_map par evar_defs (seul evar_defs est désormais exporté
par Evd). Ça s'accompagne de quelques autres modifications de
l'interface (certaines fonctions étaient des doublons, ou des
conversions entre evar_map et evar_defs).
J'ai modifié un peu la structure de evd.ml aussi, pour éviter des
fonctions redéfinies deux fois (i.e. définies trois fois !), j'ai
introduit des sous-modules pour les différentes couches.
Il y a à l'heure actuelle une pénalité en performance assez sévère (due
principalement à la nouvelle mouture de Evd.merge, si mon diagnostique
est correct). Mais fera l'objet de plusieurs optimisations dans les
commits à venir.
Un peu plus ennuyeux, la test-suite du mode déclaratif ne passe plus. Un
appel de Decl_proof_instr.mark_as_done visiblement, je suis pour
l'instant incapable de comprendre ce qui cause cette erreur. J'espère
qu'on pourra le déterminer rapidement.
Ce commit est le tout premier commit dans le trunk en rapport avec les
évolution futures de la machine de preuve, en vue en particulier
d'obtenir un "vrai refine".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11939 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
-rw-r--r-- | interp/constrintern.ml | 12 | ||||
-rw-r--r-- | interp/implicit_quantifiers.ml | 2 |
2 files changed, 7 insertions, 7 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 87768c419..a447fbe8d 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1255,7 +1255,7 @@ let interp_open_constr_patvar sigma env c = ) | _ -> map_rawconstr patvar_to_evar r in let raw = patvar_to_evar raw in - Default.understand_tcc (Evd.evars_of !sigma) env raw + Default.understand_tcc ( !sigma) env raw let interp_constr_judgment sigma env c = Default.understand_judgment sigma env (intern_constr sigma env c) @@ -1268,12 +1268,12 @@ let interp_constr_evars_gen_impls ?evdref let imps = Implicit_quantifiers.implicits_of_rawterm c in Default.understand_gen kind Evd.empty env c, imps | Some evdref -> - let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in + let c = intern_gen (kind=IsType) ~impls ( !evdref) env c in let imps = Implicit_quantifiers.implicits_of_rawterm c in Default.understand_tcc_evars evdref env kind c, imps let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c = - let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in + let c = intern_gen (kind=IsType) ~impls ( !evdref) env c in Default.understand_tcc_evars evdref env kind c let interp_casted_constr_evars_impls ?evdref @@ -1294,7 +1294,7 @@ let interp_type_evars evdref env ?(impls=([],[])) c = let interp_constr_judgment_evars evdref env c = Default.understand_judgment_tcc evdref env - (intern_constr (Evd.evars_of !evdref) env c) + (intern_constr ( !evdref) env c) type ltac_sign = identifier list * unbound_ltac_var_map @@ -1324,7 +1324,7 @@ let interp_binder sigma env na t = Default.understand_type sigma env t' let interp_binder_evars evdref env na t = - let t = intern_gen true (Evd.evars_of !evdref) env t in + let t = intern_gen true ( !evdref) env t in let t' = locate_if_isevar (loc_of_rawconstr t) na t in Default.understand_tcc_evars evdref env IsType t' @@ -1371,7 +1371,7 @@ let interp_context ?(fail_anonymous=false) sigma env params = (Default.understand_judgment sigma) env bl let interp_context_evars ?(fail_anonymous=false) evdref env params = - let bl = intern_context fail_anonymous (Evd.evars_of !evdref) env params in + let bl = intern_context fail_anonymous ( !evdref) env params in interp_context_gen (fun env t -> Default.understand_tcc_evars evdref env IsType t) (Default.understand_judgment_tcc evdref) env bl diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index d48c85616..a9d370447 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -149,7 +149,7 @@ let free_vars_of_rawconstr ?(bound=Idset.empty) = let rec make_fresh ids env x = if is_freevar ids env x then x else make_fresh ids env (Nameops.lift_ident x) -let freevars_of_ids env ids = +let fre_ids env ids = List.filter (is_freevar env (Global.env())) ids let next_ident_away_from id avoid = make_fresh avoid (Global.env ()) id |