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

7 files changed, 93 insertions, 96 deletions

diff --git a/.depend b/.depend
index d09a4d418f..aaf9e30500 100644
--- a/.depend
+++ b/.depend
@@ -741,12 +741,14 @@ kernel/cooking.cmx: lib/util.cmx kernel/typeops.cmx kernel/term.cmx \
     kernel/sign.cmx kernel/reduction.cmx lib/pp.cmx kernel/names.cmx \
     kernel/environ.cmx kernel/declarations.cmx kernel/cemitcodes.cmx \
     kernel/cooking.cmi 
-kernel/csymtable.cmo: kernel/vm.cmi kernel/term.cmi kernel/pre_env.cmi \
-    kernel/names.cmi kernel/declarations.cmi kernel/cemitcodes.cmi \
-    kernel/cbytegen.cmi kernel/cbytecodes.cmi kernel/csymtable.cmi 
-kernel/csymtable.cmx: kernel/vm.cmx kernel/term.cmx kernel/pre_env.cmx \
-    kernel/names.cmx kernel/declarations.cmx kernel/cemitcodes.cmx \
-    kernel/cbytegen.cmx kernel/cbytecodes.cmx kernel/csymtable.cmi 
+kernel/csymtable.cmo: kernel/vm.cmi kernel/term.cmi kernel/sign.cmi \
+    kernel/pre_env.cmi kernel/names.cmi kernel/environ.cmi \
+    kernel/declarations.cmi kernel/cemitcodes.cmi kernel/cbytegen.cmi \
+    kernel/cbytecodes.cmi kernel/csymtable.cmi 
+kernel/csymtable.cmx: kernel/vm.cmx kernel/term.cmx kernel/sign.cmx \
+    kernel/pre_env.cmx kernel/names.cmx kernel/environ.cmx \
+    kernel/declarations.cmx kernel/cemitcodes.cmx kernel/cbytegen.cmx \
+    kernel/cbytecodes.cmx kernel/csymtable.cmi 
 kernel/declarations.cmo: lib/util.cmi kernel/univ.cmi kernel/term.cmi \
     kernel/sign.cmi lib/rtree.cmi kernel/names.cmi kernel/mod_subst.cmi \
     kernel/cemitcodes.cmi kernel/cbytecodes.cmi kernel/declarations.cmi 
@@ -759,12 +761,10 @@ kernel/entries.cmx: kernel/univ.cmx kernel/term.cmx kernel/sign.cmx \
     kernel/names.cmx kernel/entries.cmi 
 kernel/environ.cmo: lib/util.cmi kernel/univ.cmi kernel/term.cmi \
     kernel/sign.cmi kernel/pre_env.cmi kernel/names.cmi \
-    kernel/declarations.cmi kernel/csymtable.cmi kernel/cbytegen.cmi \
-    kernel/environ.cmi 
+    kernel/declarations.cmi kernel/cbytegen.cmi kernel/environ.cmi 
 kernel/environ.cmx: lib/util.cmx kernel/univ.cmx kernel/term.cmx \
     kernel/sign.cmx kernel/pre_env.cmx kernel/names.cmx \
-    kernel/declarations.cmx kernel/csymtable.cmx kernel/cbytegen.cmx \
-    kernel/environ.cmi 
+    kernel/declarations.cmx kernel/cbytegen.cmx kernel/environ.cmi 
 kernel/esubst.cmo: lib/util.cmi kernel/esubst.cmi 
 kernel/esubst.cmx: lib/util.cmx kernel/esubst.cmi 
 kernel/indtypes.cmo: lib/util.cmi kernel/univ.cmi kernel/typeops.cmi \
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index fc2d092547..d81b98ac47 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 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)
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 8ba5962d3b..96c2ba2761 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 7bf7a8901b..7a7e00e905 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 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 *)
 
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)