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 /kernel/environ.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 'kernel/environ.mli')
| -rw-r--r-- | kernel/environ.mli | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index 5fa5f56740..175b18b247 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -195,11 +195,6 @@ val compile_constant_body : env -> constr_substituted option -> bool -> bool -> Cemitcodes.body_code (* opaque *) (* boxed *) -(*s Functions for proofs/logic.ml *) -val clear_hyps : - variable list -> (variable list -> named_declaration -> unit) -> - named_context_val -> named_context_val * variable list - exception Hyp_not_found (* [apply_to_hyp sign id f] split [sign] into [tail::(id,_,_)::head] and @@ -221,3 +216,6 @@ val apply_to_hyp_and_dependent_on : named_context_val -> variable -> val insert_after_hyp : named_context_val -> variable -> named_declaration -> (named_context -> unit) -> named_context_val + +val remove_hyps : identifier list -> (named_declaration -> named_declaration) -> named_context_val -> named_context_val * identifier list + |