diff options
| author |  notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-03-27 11:53:33 +0000 |
|---|---|---|
| committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-03-27 11:53:33 +0000 |
| commit | da5b8113b2433cce5725edbb69d55bfcf4b4cbe4 (patch) | |
| tree | 4fe83fb60475c0a099cb2cfd2316ce3a603d8287 /interp | |
| 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 'interp')
0 files changed, 0 insertions, 0 deletions