From 2f5c0f8880cd4ccc27cef4980768d35c9ebd26ea Mon Sep 17 00:00:00 2001
From: mohring
Date: Wed, 2 Nov 2005 22:12:16 +0000
Subject: Types inductifs parametriques

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7493 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/coq.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'ide')

diff --git a/ide/coq.ml b/ide/coq.ml
index 0a72c97bc4..eeb31e1ae2 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -432,10 +432,8 @@ let make_cases s =
   let glob_ref = Nametab.locate qualified_name in
   match glob_ref with
     | Libnames.IndRef i -> 
-	let _,
-	{
-	  Declarations.mind_nparams = np ;
-	  Declarations.mind_consnames = carr ;
+	let {Declarations.mind_nparams = np},
+	{Declarations.mind_consnames = carr ;
 	 Declarations.mind_nf_lc = tarr } 
 	= Global.lookup_inductive i 
 	in
-- 
cgit v1.2.3