diff options
| author | notin | 2007-01-22 18:06:35 +0000 |
|---|---|---|
| committer | notin | 2007-01-22 18:06:35 +0000 |
| commit | 90a2cea28df5ecdf9e2cdc4351aad5f6a993a003 (patch) | |
| tree | b9994cf9ff1163facd312b96918d929f5e0ff7ae /pretyping/evarutil.mli | |
| parent | 612ea3d4b3c7d7e00616b009050803cd7b7f763e (diff) | |
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
Diffstat (limited to 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 670b742707..9ad7b6e589 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -158,3 +158,10 @@ val whd_castappevar : evar_map -> constr -> constr val pr_tycon_type : env -> type_constraint_type -> Pp.std_ppcmds val pr_tycon : env -> type_constraint -> Pp.std_ppcmds + + +(**********************************) +(* Removing hyps in evars'context *) +val clear_evar_hyps_in_evar : evar_defs ref -> evar -> constr array -> identifier list -> constr +val clear_evar_hyps_in_constr : evar_defs ref -> constr -> identifier list -> constr +val clear_evar_hyps : evar_map -> evar_info -> identifier list -> evar_info * evar_map |