From 296faec482d17f9bfdc419f79ed565ecd8035e60 Mon Sep 17 00:00:00 2001
From: barras
Date: Thu, 7 Feb 2002 16:07:34 +0000
Subject: petit nettoyage de kernel/inductive

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2460 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 ce62acdf8f..9d63dc7dd3 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -282,7 +282,7 @@ let check_branch_types env cj (lft,explft) =
 let judge_of_case env ci pj cj lfj =
   let indspec =
     try find_rectype env cj.uj_type
-    with Induc -> error_case_not_inductive env cj in
+    with Not_found -> error_case_not_inductive env cj in
   let _ = check_case_info env (fst indspec) ci in
   let (bty,rslty,univ) =
     type_case_branches env indspec pj cj.uj_val in
-- 
cgit v1.2.3