diff options
| author | notin | 2007-03-27 11:53:33 +0000 |
|---|---|---|
| committer | notin | 2007-03-27 11:53:33 +0000 |
| commit | da5b8113b2433cce5725edbb69d55bfcf4b4cbe4 (patch) | |
| tree | 4fe83fb60475c0a099cb2cfd2316ce3a603d8287 /kernel/environ.mli | |
| parent | b1ef4a82d936a6c56facd58daf9c513f44d7fb8e (diff) | |
Modification de la vm:
- le type val_kind n'embarque plus le constr (pb de cohérence avec
le context);
- en revanche, lors du calcul d'une valeur, on calcule aussi
l'ensemble des variables nommées dont la valeur peut dépendre;
- lors du clear_hyps, si la valeur dépend d'une variable effacée, on
invalide le calcul.
Corrige le bug #1419
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9733 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/environ.mli')
| -rw-r--r-- | kernel/environ.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index 8ba5962d3b..96c2ba2761 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -35,6 +35,7 @@ open Sign type env val pre_env : env -> Pre_env.env +val env_of_pre_env : Pre_env.env -> env type named_context_val val eq_named_context_val : named_context_val -> named_context_val -> bool @@ -216,5 +217,5 @@ 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 +val remove_hyps : identifier list -> (named_declaration -> named_declaration) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val * identifier list |