From f62385a60b4d4f20a95891b6044c7bc9135b5915 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sun, 1 Oct 2000 13:50:11 +0000
Subject: Code comateux

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

(limited to 'kernel')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index ad1ac931e..84b5b7a07 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -103,6 +103,7 @@ let rec whd_state (x, stack as s) =
     | _             -> s
 
 let whd_stack x = appterm_of_stack (whd_state (x, empty_stack))
+let whd_castapp_stack = whd_stack
 
 let stack_reduction_of_reduction red_fun env sigma s =
   let t = red_fun env sigma (app_stack s) in
@@ -1186,7 +1187,7 @@ let rec whd_ise1 sigma c =
 	whd_ise1 sigma (existential_value sigma (ev,args))
     | IsCast (c,_) -> whd_ise1 sigma c
     (* A quoi servait cette ligne ???
-    | DOP0(Sort(Type _)) -> DOP0(Sort(Type dummy_univ))
+    | IsSort (Type _) -> mkSort (Type dummy_univ)
     *)
     | _ -> c
 
-- 
cgit v1.2.3