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

5 files changed, 66 insertions, 81 deletions

diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index fc2d09254..d81b98ac4 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -121,31 +121,36 @@ let rec slot_for_getglobal env kn =
     rk := Some pos;
     pos
 
-and slot_for_fv env fv=
+and slot_for_fv env fv =
   match fv with
   | FVnamed id -> 
-      let nv = lookup_named_val id env in
+      let nv = Pre_env.lookup_named_val id env in
       begin
 	match !nv with
-	| VKvalue v -> v
-	| VKaxiom id ->
-	    let v = val_of_named id in
-	    nv := VKvalue v; v
-	| VKdef c ->
-	    let v = val_of_constr (env_of_named id env) c in
-	    nv := VKvalue v; v
+	| VKvalue (v,_) -> v
+	| VKnone -> 
+	    let (_, b, _) = Sign.lookup_named id env.env_named_context in
+	    let v,d = 
+	      match b with
+		| None -> (val_of_named id, Idset.empty)
+		| Some c -> (val_of_constr env c, Environ.global_vars_set (Environ.env_of_pre_env env) c)
+	    in
+	      nv := VKvalue (v,d); v
       end
   | FVrel i ->
-      let rv = lookup_rel_val i env in
+      let rv = Pre_env.lookup_rel_val i env in
       begin
 	match !rv with
-	| VKvalue v -> v
-	| VKaxiom k ->
-	    let v = val_of_rel k in
-	    rv := VKvalue v; v
-	| VKdef c ->
-	    let v = val_of_constr (env_of_rel i env) c in
-	    rv := VKvalue v; v
+	| VKvalue (v, _) -> v
+	| VKnone -> 
+	    let (_, b, _) = Sign.lookup_rel i env.env_rel_context in
+	    let (v, d) =
+	      match b with 
+		| None -> (val_of_rel i, Idset.empty)
+		| Some c -> let renv =  env_of_rel i env in
+			      (val_of_constr renv c, Environ.global_vars_set (Environ.env_of_pre_env renv) c)
+	    in
+	      rv := VKvalue (v,d); v
       end
  
 and eval_to_patch env (buff,pl,fv) = 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 56c057488..a9ba253b0 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)
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 8ba5962d3..96c2ba276 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
 
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 7bf7a8901..7a7e00e90 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -33,25 +33,20 @@ 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_rel_val       : lazy_val list;
   env_nb_rel        : int;
   env_stratification : stratification }
 
@@ -78,18 +73,13 @@ let empty_env = {
 (* Rel context *)
 
 let nb_rel env = env.env_nb_rel
-
+  
 let push_rel d env =
-  let _,body,_ = d in
-  let rval =
-    match body with
-    | None -> ref (VKaxiom env.env_nb_rel)
-    | Some c -> ref (VKdef c)
-  in     
-  { env with
-    env_rel_context = add_rel_decl d env.env_rel_context;
-    env_rel_val = rval :: env.env_rel_val;
-    env_nb_rel = env.env_nb_rel + 1 }
+  let rval = ref VKnone in
+    { env with
+      env_rel_context = add_rel_decl d env.env_rel_context;
+      env_rel_val = rval :: env.env_rel_val;
+      env_nb_rel = env.env_nb_rel + 1 }
  
 let lookup_rel_val n env =
   try List.nth env.env_rel_val (n - 1)
@@ -101,16 +91,13 @@ let env_of_rel n env =
     env_rel_val = Util.list_skipn n env.env_rel_val;
     env_nb_rel = env.env_nb_rel - n
   }
-
+    
 (* Named context *)
 
 let push_named_context_val d (ctxt,vals) =
-  let id,body,_ = d in
-  let rval =
-    match body with
-    | None -> ref (VKaxiom id)
-    | Some c -> ref (VKdef c)
-  in Sign.add_named_decl d ctxt, (id,rval)::vals
+  let id,_,_ = d in
+  let rval = ref VKnone in
+    Sign.add_named_decl d ctxt, (id,rval)::vals
 
 exception ASSERT of Sign.rel_context
 
@@ -118,18 +105,14 @@ let push_named d env =
 (*  if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context);
   assert (env.env_rel_context = []); *)
   let id,body,_ = d in
-  let rval =
-    match body with
-    | None -> ref (VKaxiom id)
-    | Some c -> ref (VKdef c)
-  in
-  { env with  
-    env_named_context = Sign.add_named_decl d env.env_named_context;
-    env_named_vals =  (id,rval):: env.env_named_vals }
+  let rval = ref VKnone in
+    { env with  
+      env_named_context = Sign.add_named_decl d env.env_named_context;
+      env_named_vals =  (id,rval):: env.env_named_vals }
 
 let lookup_named_val id env =
-   snd(List.find (fun (id',_) -> id = id') env.env_named_vals)
-  
+  snd(List.find (fun (id',_) -> id = id') env.env_named_vals)
+    
 (* Warning all the names should be different *)
 let env_of_named id env = env
  
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 6144f20cb..728f28be0 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 *)