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.ml | |
| 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.ml')
| -rw-r--r-- | kernel/environ.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 56c0574888..a9ba253b0d 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -15,7 +15,6 @@ open Univ open Term open Declarations open Pre_env -open Csymtable (* The type of environments. *) @@ -24,6 +23,7 @@ type named_context_val = Pre_env.named_context_val type env = Pre_env.env let pre_env env = env +let env_of_pre_env env = env let empty_named_context_val = empty_named_context_val @@ -359,14 +359,15 @@ let insert_after_hyp (ctxt,vals) id d check = in aux ctxt vals (* To be used in Logic.clear_hyps *) -let remove_hyps ids check (ctxt, vals) = +let remove_hyps ids check_context check_value (ctxt, vals) = let ctxt,vals,rmv = - List.fold_right2 (fun (id,_,_ as d) v (ctxt,vals,rmv) -> + List.fold_right2 (fun (id,_,_ as d) (id',v) (ctxt,vals,rmv) -> if List.mem id ids then (ctxt,vals,id::rmv) else - let nd = check d in - (nd::ctxt,v::vals,rmv)) + let nd = check_context d in + let nv = check_value v in + (nd::ctxt,(id',nv)::vals,rmv)) ctxt vals ([],[],[]) in ((ctxt,vals),rmv) |