From 7f7fa0184ea32c81e77d34683bca8e456b80a19a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 11 Oct 2000 20:03:05 +0000
Subject: Renommage des find_m*type

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@693 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/inductive.ml  | 4 ++--
 kernel/inductive.mli | 8 ++++----
 proofs/logic.ml      | 6 +++---
 3 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 257305b006..1f1312887e 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -198,14 +198,14 @@ let find_mrectype env sigma c =
     | IsMutInd ind -> (ind, l)
     | _ -> raise Induc
 
-let find_minductype env sigma c =
+let find_inductive env sigma c =
   let (t, l) = whd_betadeltaiota_stack env sigma c in
   match kind_of_term t with
     | IsMutInd ((sp,i),_ as ind)
         when mind_type_finite (lookup_mind sp env) i -> (ind, l)
     | _ -> raise Induc
 
-let find_mcoinductype env sigma c =
+let find_coinductive env sigma c =
   let (t, l) = whd_betadeltaiota_stack env sigma c in
   match kind_of_term t with
     | IsMutInd ((sp,i),_ as ind)
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 4f27c30b88..45542ddc3c 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -139,14 +139,14 @@ exception Induc
 val extract_mrectype  : constr -> inductive * constr list
 
 (* [find_m*type env sigma c] coerce [c] to an recursive type (I args).
-   [find_mrectype], [find_minductype] and [find_mcoinductype]
+   [find_rectype], [find_inductive] and [find_coinductive]
    respectively accepts any recursive type, only an inductive type and
    only a coinductive type.
    They raise [Induc] if not convertible to a recursive type. *)
 
-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
+val find_mrectype    : env -> 'a evar_map -> constr -> inductive * constr list
+val find_inductive   : env -> 'a evar_map -> constr -> inductive * constr list
+val find_coinductive : env -> 'a evar_map -> constr -> inductive * constr list
 
 val lookup_mind_specif : inductive -> env -> inductive_instance
 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 9aeff1f28a..0e5b970c90 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -355,7 +355,7 @@ let prim_refiner r sigma goal =
             | IsProd (_,c1,b) -> 
             	if k = 1 then 
 		  try 
-		    let _ = find_minductype env sigma c1 in ()
+		    let _ = find_inductive env sigma c1 in ()
 		  with Induc -> 
 		    error "cannot do a fixpoint on a non inductive type"
             	else 
@@ -375,7 +375,7 @@ let prim_refiner r sigma goal =
             | IsProd (_,c1,b) -> 
             	if k = 1 then 
 		  try 
-		    fst (find_minductype env sigma c1)
+		    fst (find_inductive env sigma c1)
 		  with Induc -> 
 		    error "cannot do a fixpoint on a non inductive type"
             	else 
@@ -407,7 +407,7 @@ let prim_refiner r sigma goal =
             | IsProd (_,c1,b) -> check_is_coind  b
             | _ -> 
 		try 
-		  let _ = find_mcoinductype env sigma b in ()
+		  let _ = find_coinductive env sigma b in ()
                 with Induc -> 
 		  error ("All methods must construct elements " ^
 			  "in coinductive types")
-- 
cgit v1.2.3