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
---
 pretyping/cases.ml     | 8 ++++----
 pretyping/pretyping.ml | 2 +-
 pretyping/retyping.ml  | 2 +-
 3 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index fd6a0457d..2fbfa70f7 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -190,7 +190,7 @@ type 'a pattern_matching_problem =
 (* Utils *)
 
 let to_mutind env sigma t =
-  try IsInd (t,try_mutind_of env sigma t)
+  try IsInd (t,find_inductive env sigma t)
   with Induc -> NotInd t
 
 let type_of_tomatch_type = function
@@ -831,18 +831,18 @@ let coerce_row typing_fun isevars env row tomatch =
 	  (let tyi = inductive_of_rawconstructor c in
 	   try 
 	     let indtyp = inh_coerce_to_ind isevars env j.uj_type tyi in
-	     IsInd (j.uj_type,try_mutind_of env !isevars j.uj_type)
+	     IsInd (j.uj_type,find_inductive env !isevars j.uj_type)
 	 with NotCoercible ->
 	   (* 2 cas : pas le bon inductive ou pas un inductif du tout *)
 	   try
-	     let ind_data = try_mutind_of env !isevars j.uj_type in
+	     let ind_data = find_inductive env !isevars j.uj_type in
 	     error_bad_constructor_loc cloc CCI
 	       (constructor_of_rawconstructor c) ind_data.mind
 	   with Induc ->
 	     error_case_not_inductive_loc
 	       (loc_of_rawconstr tomatch) CCI env j.uj_val j.uj_type)
       | None -> 
-	  try IsInd (j.uj_type,try_mutind_of env !isevars j.uj_type)
+	  try IsInd (j.uj_type,find_inductive env !isevars j.uj_type)
 	  with Induc -> NotInd (j.uj_type)
   in (j.uj_val,t)
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 8462a72f6..340129813 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -397,7 +397,7 @@ match cstr with   (* O
 | ROldCase (loc,isrec,po,c,lf) ->
   let cj = pretype empty_tycon env isevars lvar lmeta c in
   let {mind=mind;params=params;realargs=realargs} =
-    try try_mutind_of env !isevars cj.uj_type
+    try find_inductive env !isevars cj.uj_type
     with Induc -> error_case_not_inductive CCI env
 	(nf_ise1 !isevars cj.uj_val) (nf_ise1 !isevars cj.uj_type) in
   let pj = match po with
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 67c131524..0e61614b3 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -53,7 +53,7 @@ let rec type_of env cstr=
         let (typ,kind) = destCast (type_of_constructor env sigma cstr) in typ
     | IsMutCase (_,p,c,lf) ->
         let ind_data =
-          try try_mutind_of env sigma (type_of env c)
+          try find_inductive env sigma (type_of env c)
           with Induc -> anomaly "type_of: Bad inductive" in
 	let (aritysign,_) = get_arity env sigma ind_data in
 	let (psign,_) = splay_prod env sigma (type_of env p) in
-- 
cgit v1.2.3