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 /pretyping | |
| 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 'pretyping')
| -rw-r--r-- | pretyping/evarutil.ml | 22 |
1 files changed, 17 insertions, 5 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 54e84db86f..99aa440b3f 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -16,6 +16,7 @@ open Univ open Term open Termops open Sign +open Pre_env open Environ open Evd open Reductionops @@ -367,7 +368,7 @@ and clear_hyps_in_evi evd evi ids = let nconcl = try check_and_clear_in_constr evd (evar_concl evi) ids with Dependency_error id' -> error (string_of_id id' ^ " is used in conclusion") in let (nhyps,_) = - let aux (id,ob,c) = + let check_context (id,ob,c) = try (id, (match ob with @@ -375,13 +376,24 @@ and clear_hyps_in_evi evd evi ids = | Some b -> Some (check_and_clear_in_constr evd b ids)), check_and_clear_in_constr evd c ids) with Dependency_error id' -> error (string_of_id id' ^ " is used in hypothesis " - ^ string_of_id id) + ^ string_of_id id) in - remove_hyps ids aux (evar_hyps evi) + let check_value vk = + match !vk with + | VKnone -> vk + | VKvalue (v,d) -> + if (List.for_all (fun e -> not (Idset.mem e d)) ids) then + (* v does depend on any of ids, it's ok *) + vk + else + (* v depends on one of the cleared hyps: we forget the computed value *) + ref VKnone + in + remove_hyps ids check_context check_value (evar_hyps evi) in { evi with - evar_concl = nconcl; - evar_hyps = nhyps} + evar_concl = nconcl; + evar_hyps = nhyps} let need_restriction k args = not (array_for_all (closedn k) args) |