From 1c6747af716224b092b0f197772bc6bcc186293b Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 4 May 2000 16:58:33 +0000
Subject: Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@416 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/indrec.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/indrec.ml b/library/indrec.ml
index b764f6cf7..3b02d092c 100644
--- a/library/indrec.ml
+++ b/library/indrec.ml
@@ -438,7 +438,7 @@ let type_mutind_rec env sigma indspec pt p c =
 
 let type_rec_branches recursive env sigma ct pt p c =
   try
-    let indspec = try_mutind_of env sigma ct in
+    let indspec = find_inductive env sigma ct in
     if recursive then 
       type_mutind_rec env sigma indspec  pt p c
     else 
-- 
cgit v1.2.3