From 8fc99285ff74272185c53859b1ba21279deb624b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 23 Oct 2000 08:25:31 +0000
Subject: Simplifications/questions

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

(limited to 'kernel')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 539426bc3e..d279351876 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -889,8 +889,6 @@ and eqappr cv_pb infos appr1 appr2 =
 
 
 let fconv cv_pb env sigma t1 t2 =
-  let t1 = local_strong strip_outer_cast t1
-  and t2 = local_strong strip_outer_cast t2 in
   if eq_constr t1 t2 then 
     Constraint.empty
   else
@@ -1154,7 +1152,7 @@ let rec whd_ise sigma c =
           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)
+(*  | IsSort (Type _) -> mkSort (Type dummy_univ)*)
   | _ -> c
 
 
-- 
cgit v1.2.3