diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-16 13:45:20 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-16 13:45:20 +0000 |
| commit | 2d55be3f00e6fbc4ff91c4d3138dca2d68db587b (patch) | |
| tree | 2c4003d0b4cc5c212ddf78f8f67dd7e8bece6c45 /parsing | |
| parent | b7e6df6ff46c2eaad9cd6a0f1f0d21bc0c3b4c61 (diff) | |
Bug Search
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4644 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/search.ml | 1 |
1 files changed, 1 insertions, 0 deletions
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 |