From 6b3ac9bca3082fabee95bdd492d8cd9e26de7a0e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 26 Oct 2000 13:17:49 +0000
Subject: Suppression cas Cast dans whd_ise et whd_ise1; Suppression du cast au
 moment de l'instanciation des Meta dans plain_instance

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@769 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/reduction.ml | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

(limited to 'kernel')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 5ec58c1672..5af00238f3 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -928,6 +928,8 @@ let whd_meta metamap c = match kind_of_term c with
 let plain_instance s c = 
   let rec irec u = match kind_of_term u with
     | IsMeta p -> (try List.assoc p s with Not_found -> u)
+    | IsCast (m,_) when isMeta m ->
+	(try List.assoc (destMeta m) s with Not_found -> u)
     | _ -> map_constr irec u
   in 
   if s = [] then c else irec c
@@ -1148,8 +1150,6 @@ let rec whd_ise sigma c =
 	if Evd.is_defined sigma ev then
           whd_ise sigma (existential_value sigma (ev,args))
 	else raise (Uninstantiated_evar ev)
-  | IsCast (c,_) -> whd_ise sigma c
-(*  | IsSort (Type _) -> mkSort (Type dummy_univ)*)
   | _ -> c
 
 
@@ -1158,10 +1158,6 @@ let rec whd_ise1 sigma c =
   match kind_of_term c with
     | IsEvar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev ->
 	whd_ise1 sigma (existential_value sigma (ev,args))
-    | IsCast (c,_) -> whd_ise1 sigma c
-    (* A quoi servait cette ligne ???
-    | IsSort (Type _) -> mkSort (Type dummy_univ)
-    *)
     | _ -> c
 
 let nf_ise1 sigma = local_strong (whd_ise1 sigma)
-- 
cgit v1.2.3