From 7f2aa8490291da690d4367a3be795fcbea3f6fdc Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 10 Jun 2003 21:15:09 +0000
Subject: Simplification case_info

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4124 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/inductiveops.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 2da3748d5d..a64c553899 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -88,10 +88,9 @@ let mis_constr_nargs_env env (kn,i) =
 let make_case_info env ind style pats_source =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   let print_info =
-    { cnames    = mip.mind_consnames;
-      ind_nargs = mip.mind_nrealargs;
+    { ind_nargs = mip.mind_nrealargs;
       style     = style;
-      source    =pats_source } in
+      source    = pats_source } in
   { ci_ind     = ind;
     ci_npar    = mip.mind_nparams;
     ci_pp_info = print_info }
-- 
cgit v1.2.3