From 7da855f0e3ed56aa9ad9149f6ef95be11f7ec5d2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 1 Jul 2000 10:15:38 +0000
Subject: Extension de find_inductive aux co-inductifs et renommage en
 find_rectype

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@542 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/pretyping.ml | 4 ++--
 pretyping/retyping.ml  | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 65e4e76ff9..41b9d10695 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -360,7 +360,7 @@ match cstr with   (* O
 | ROldCase (loc,isrec,po,c,lf) ->
   let cj = pretype empty_tycon env isevars lvar lmeta c in
   let (IndType (indf,realargs) as indt) = 
-    try find_inductive env !isevars (body_of_type cj.uj_type)
+    try find_rectype env !isevars (body_of_type cj.uj_type)
     with Induc -> error_case_not_inductive CCI env
 	(nf_ise1 !isevars cj.uj_val) (nf_ise1 !isevars (body_of_type cj.uj_type)) in
   let pj = match po with
@@ -393,7 +393,7 @@ match cstr with   (* O
 	      with UserError _ -> findtype (i+1) in
 	    findtype 0 in
 
-  let evalct = find_inductive env !isevars (body_of_type cj.uj_type) (*Pour normaliser evars*)
+  let evalct = find_rectype env !isevars (body_of_type cj.uj_type) (*Pour normaliser evars*)
   and evalPt = nf_ise1 !isevars (body_of_type pj.uj_type) in
 
   let (bty,rsty) =
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 9398d40f91..535a0c5836 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -52,8 +52,8 @@ let rec type_of env cstr=
     | IsMutConstruct cstr -> body_of_type (type_of_constructor env sigma cstr)
     | IsMutCase (_,p,c,lf) ->
         let IndType (indf,realargs) =
-          try find_inductive env sigma (type_of env c)
-          with Induc -> anomaly "type_of: Bad inductive" in
+          try find_rectype env sigma (type_of env c)
+          with Induc -> anomaly "type_of: Bad recursive type" in
 	let (aritysign,_) = get_arity env sigma indf in
 	let (psign,_) = splay_prod env sigma (type_of env p) in
         let al =
-- 
cgit v1.2.3