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
---
 proofs/logic.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'proofs')

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