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/environ.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'kernel/environ.ml')

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