From 7da855f0e3ed56aa9ad9149f6ef95be11f7ec5d2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 1 Jul 2000 10:15:38 +0000
Subject: Extension de find_inductive aux co-inductifs et renommage en
 find_rectype

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

(limited to 'proofs')

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 5f8d7c2f2c..c045ee73af 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -124,7 +124,7 @@ and mk_casegoals sigma goal goalacc p c =
   let (acc',ct) = mk_hdgoals sigma goal goalacc c in 
   let (acc'',pt) = mk_hdgoals sigma goal acc' p in
   let indspec =
-    try find_inductive env sigma ct
+    try find_rectype env sigma ct
     with Induc -> anomaly "mk_casegoals" in
   let (lbrty,conclty) = type_case_branches env sigma indspec pt p c in
   (acc'',lbrty,conclty)
-- 
cgit v1.2.3