From 1c6747af716224b092b0f197772bc6bcc186293b Mon Sep 17 00:00:00 2001
From: herbelin
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
---
 kernel/reduction.ml  | 4 ++--
 kernel/reduction.mli | 4 ++--
 kernel/typeops.ml    | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'kernel')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index eb84a2a0f3..ec4dc3cc30 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -1152,8 +1152,8 @@ let find_mcoinductype env sigma c =
     | _ -> raise Induc
 
 (* raise Induc if not an inductive type *)
-let try_mutind_of env sigma ty =
-  let (mind,largs) = find_mrectype env sigma ty in
+let find_inductive env sigma ty =
+  let (mind,largs) = find_minductype 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
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 583a7cf1ff..25adf3b889 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -210,10 +210,10 @@ val find_mrectype     : env -> 'a evar_map -> constr -> inductive * constr list
 val find_minductype   : env -> 'a evar_map -> constr -> inductive * constr list
 val find_mcoinductype : env -> 'a evar_map -> constr -> inductive * constr list
 
-(* [try_mutind_of env sigma t] raises [Induc] if [t] is not an inductive type*)
+(* [find_inductive env sigma t] raises [Induc] if [t] is not an inductive type*)
 (* The resulting summary is relative to the current env *)
 open Inductive
-val try_mutind_of : env -> 'a evar_map -> constr -> inductive_summary
+val find_inductive : env -> 'a evar_map -> constr -> inductive_summary
 
 val get_constructors : env -> 'a evar_map -> inductive_summary
       -> constructor_summary array
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index c887116351..4a89568dcb 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -319,7 +319,7 @@ let check_branches_message env sigma (c,ct) (explft,lft) =
 let type_of_case env sigma ci pj cj lfj =
   let lft = Array.map (fun j -> j.uj_type) lfj in
   let indspec =
-    try try_mutind_of env sigma cj.uj_type
+    try find_inductive env sigma cj.uj_type
     with Induc -> error_case_not_inductive CCI env cj.uj_val cj.uj_type in
   let (bty,rslty) =
     type_case_branches env sigma indspec pj.uj_type pj.uj_val cj.uj_val in
-- 
cgit v1.2.3