diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 3d5fa57bb..33428af02 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1612,7 +1612,7 @@ let interp_search_about_item env = as an identifier component") let vernac_search s gopt r = - let g = un_opt gopt 1 in + let g = Option.default 1 gopt in let r = interp_search_restriction r in let env = try snd (Pfedit.get_goal_context g) |