From 3dc7ac2dcfdf8e8255a23c868de29a03a11ceb2e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 1 Oct 2000 13:37:35 +0000
Subject: Plus de whd_castapp

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@624 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/logic.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 3b7c85b405..77c6a996ef 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -359,7 +359,7 @@ let prim_refiner r sigma goal =
     | { name = Fix; hypspecs = []; terms = []; 
 	newids = [f]; params = [Num(_,n)] } ->
      	let rec check_ind k cl = 
-          match kind_of_term (whd_castapp cl) with 
+          match kind_of_term (strip_outer_cast cl) with 
             | IsProd (_,c1,b) -> 
             	if k = 1 then 
 		  try 
@@ -379,7 +379,7 @@ let prim_refiner r sigma goal =
     
     | { name = Fix; hypspecs = []; terms = lar; newids = lf; params = ln } ->
      	let rec check_ind k cl = 
-          match kind_of_term (whd_castapp cl) with 
+          match kind_of_term (strip_outer_cast cl) with 
             | IsProd (_,c1,b) -> 
             	if k = 1 then 
 		  try 
@@ -410,7 +410,7 @@ let prim_refiner r sigma goal =
 
     | { name = Cofix; hypspecs = []; terms = lar; newids = lf; params = [] } ->
      	let rec check_is_coind cl = 
-	  let b = whd_betadeltaiota env sigma (whd_castapp cl) in
+	  let b = whd_betadeltaiota env sigma cl in
           match kind_of_term b with
             | IsProd (_,c1,b) -> check_is_coind  b
             | _ -> 
-- 
cgit v1.2.3