diff options
Diffstat (limited to 'parsing/search.ml')
| -rw-r--r-- | parsing/search.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/search.ml b/parsing/search.ml index da57d9002..84022e7b1 100644 --- a/parsing/search.ml +++ b/parsing/search.ml @@ -80,7 +80,7 @@ let gen_crible refopt (fn : global_reference -> env -> constr -> unit) = | _ -> () in try - Declaremods.iter_all_segments false crible_rec + Declaremods.iter_all_segments crible_rec with Not_found -> () |