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
---
 kernel/typeops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/typeops.ml')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 7edb8680f1..720061fa59 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -209,7 +209,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 -> body_of_type j.uj_type) lfj in
   let indspec =
-    try find_inductive env sigma (body_of_type cj.uj_type)
+    try find_rectype env sigma (body_of_type cj.uj_type)
     with Induc ->
       error_case_not_inductive CCI env cj.uj_val (body_of_type cj.uj_type) in
   let (bty,rslty) =
-- 
cgit v1.2.3