Correction du bug #1315:

- ajouts des opérations clear_evar_hyps_in_evar,
  clear_evar_hyps_in_constr et clear_evar_hyps dans Evarutil, qui
  permettent de supprimer des hypothèses dans le contexte des evars, 
  en créant une nouvelle evar avec un contexte restreint;

- adaptation de clear_hyps dans Logic pour qu'elle mette à jour le
  contexte des evars;

- adaptation de prim_refiner pour qu'elle renvoie le evar_map modifié;

- déplacement de la tactique Change_evars dans prim_rule.



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

1 files changed, 2 insertions, 0 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index fb4321bc36..2afe4601ff 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -77,6 +77,8 @@ let is_defined sigma ev =
   let info = find sigma ev in 
   not (info.evar_body = Evar_empty)
 
+let evar_concl ev = ev.evar_concl
+let evar_hyps ev = ev.evar_hyps
 let evar_body ev = ev.evar_body
 let evar_env evd = Global.env_of_context evd.evar_hyps