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
---
 kernel/inductive.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/inductive.ml')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index a3e95abbd8..16139abfeb 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -196,8 +196,8 @@ let lookup_mind_specif ((sp,tyi),args) env =
   { mis_sp = sp; mis_mib = mib; mis_tyi = tyi; mis_args = args;
     mis_mip = mind_nth_type_packet mib tyi }
 
-let find_inductive env sigma ty =
-  let (mind,largs) = find_minductype env sigma ty in
+let find_rectype env sigma ty =
+  let (mind,largs) = find_mrectype env sigma ty in
   let mispec = lookup_mind_specif mind env in 
   let nparams = mis_nparams mispec in
   let (params,realargs) = list_chop nparams largs in
-- 
cgit v1.2.3