From bb7d7482724489521dde94a5b70af7864acfa802 Mon Sep 17 00:00:00 2001
From: barras
Date: Thu, 1 Mar 2001 10:09:34 +0000
Subject: nouvelle implantation de la reduction suppression de IsXtra du noyau

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

(limited to 'kernel/typeops.ml')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 65be6547b4..7b6e58c83c 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -679,8 +679,6 @@ let rec check_subterm_rec_meta env sigma vectn k def =
 	| IsMeta _ -> true
 
 	| IsVar _ | IsSort _ ->  List.for_all (check_rec_call env n lst) l
-
-	| IsXtra _ ->  List.for_all (check_rec_call env n lst) l
      )
 
      and check_rec_call_fix_body env n lst decr recArgsDecrArg body =
@@ -885,7 +883,7 @@ let type_fixpoint env sigma lna lar vdefj =
 let control_only_guard env sigma = 
   let rec control_rec c = match kind_of_term c with
     | IsRel _ | IsVar _    -> ()
-    | IsSort _ | IsMeta _ | IsXtra _ -> ()
+    | IsSort _ | IsMeta _ -> ()
     | IsCoFix (_,(tys,_,bds) as cofix) ->
 	check_cofix env sigma cofix;
 	Array.iter control_rec tys;
-- 
cgit v1.2.3