diff options
| author | aspiwack | 2009-02-19 19:13:50 +0000 |
|---|---|---|
| committer | aspiwack | 2009-02-19 19:13:50 +0000 |
| commit | e653b53692e2cc0bb4f84881b32d3242ea39be86 (patch) | |
| tree | 728e2a206876bf932c033a781e0552620f7f89d0 /proofs/evar_refiner.ml | |
| 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 'proofs/evar_refiner.ml')
| -rw-r--r-- | proofs/evar_refiner.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 17f63933f9..e1236bbaa8 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -23,20 +23,20 @@ open Refiner (* w_tactic pour instantiate *) let w_refine evk rawc evd = - if Evd.is_defined (evars_of evd) evk then + if Evd.is_defined ( evd) evk then error "Instantiate called on already-defined evar"; - let e_info = Evd.find (evars_of evd) evk in + let e_info = Evd.find ( evd) evk in let env = Evd.evar_env e_info in let sigma,typed_c = try Pretyping.Default.understand_tcc ~resolve_classes:false - (evars_of evd) env ~expected_type:e_info.evar_concl rawc + ( evd) env ~expected_type:e_info.evar_concl rawc with _ -> let loc = Rawterm.loc_of_rawconstr rawc in user_err_loc (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^ string_of_existential evk)) in - evar_define evk typed_c (evars_reset_evd sigma evd) + define evk typed_c (evars_reset_evd sigma evd) (* vernac command Existential *) @@ -56,4 +56,4 @@ let instantiate_pf_com n com pfts = let rawc = Constrintern.intern_constr sigma env com in let evd = create_goal_evar_defs sigma in let evd' = w_refine evk rawc evd in - change_constraints_pftreestate (evars_of evd') pfts + change_constraints_pftreestate ( evd') pfts |