From 2d55be3f00e6fbc4ff91c4d3138dca2d68db587b Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 16 Oct 2003 13:45:20 +0000
Subject: Bug Search

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

(limited to 'parsing')

diff --git a/parsing/search.ml b/parsing/search.ml
index 231656f6d..4413376cb 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -72,6 +72,7 @@ let gen_crible refopt (fn : global_reference -> env -> constr -> unit) =
 	  | Some (IndRef ((kn',tyi) as ind)) when kn=kn' ->
 	      print_constructors ind fn env
 	        (Array.length (mib.mind_packets.(tyi).mind_user_lc))
+          | Some _ -> ()
 	  | _ ->
               Array.iteri 
 	        (fun i mip -> print_constructors (kn,i) fn env
-- 
cgit v1.2.3