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
---
 pretyping/evarutil.ml | 22 +++++++++++++++++-----
 1 file changed, 17 insertions(+), 5 deletions(-)

(limited to 'pretyping')

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