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

1 files changed, 14 insertions, 19 deletions

diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 6144f20cbd..728f28be08 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -33,27 +33,22 @@ type stratification = {
   env_engagement : engagement option
 }
 
-type 'a val_kind =   
-  | VKvalue of values
-  | VKaxiom of 'a
-  | VKdef of constr
+type val_kind = 
+    | VKvalue of values * Idset.t
+    | VKnone
 
-type 'a lazy_val = 'a val_kind ref
+type lazy_val = val_kind ref
 
-type rel_val = inv_rel_key lazy_val
-
-type named_val = identifier lazy_val
-
-type named_vals = (identifier * named_val) list
+type named_vals = (identifier * lazy_val) list
 
 type env = {
-  env_globals       : globals;
-  env_named_context : named_context;
-  env_named_vals    : named_vals;
-  env_rel_context   : rel_context;
-  env_rel_val       : rel_val list;
-  env_nb_rel        : int;
-  env_stratification : stratification }
+    env_globals       : globals;
+    env_named_context : named_context;
+    env_named_vals    : named_vals;
+    env_rel_context   : rel_context;
+    env_rel_val       : lazy_val list;
+    env_nb_rel        : int;
+    env_stratification : stratification }
 
 type named_context_val = named_context * named_vals
 
@@ -65,14 +60,14 @@ val empty_env : env
 
 val nb_rel         : env -> int
 val push_rel       : rel_declaration -> env -> env
-val lookup_rel_val : int -> env -> rel_val
+val lookup_rel_val : int -> env -> lazy_val
 val env_of_rel     : int -> env -> env       
 (* Named context *)
 
 val push_named_context_val  : 
     named_declaration -> named_context_val -> named_context_val
 val push_named       : named_declaration -> env -> env
-val lookup_named_val : identifier -> env -> named_val
+val lookup_named_val : identifier -> env -> lazy_val
 val env_of_named     : identifier -> env -> env  
 (* Global constants *)