From da5b8113b2433cce5725edbb69d55bfcf4b4cbe4 Mon Sep 17 00:00:00 2001
From: notin
Date: Tue, 27 Mar 2007 11:53:33 +0000
Subject: 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
---
 kernel/csymtable.ml | 39 ++++++++++++++++++++++-----------------
 1 file changed, 22 insertions(+), 17 deletions(-)

(limited to 'kernel/csymtable.ml')

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) = 
-- 
cgit v1.2.3