diff options
| -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 |