diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/search.ml | 4 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/search.ml b/toplevel/search.ml index 9e61bc7fb7..91762c0003 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -247,11 +247,11 @@ let interface_search flags = extract_flags ((regexp, b) :: name) tpe subtpe mods blacklist l | (Interface.Type_Pattern s, b) :: l -> let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in - let (_, pat) = Constrintern.intern_constr_pattern Evd.empty env constr in + let (_, pat) = Constrintern.intern_constr_pattern env constr in extract_flags name ((pat, b) :: tpe) subtpe mods blacklist l | (Interface.SubType_Pattern s, b) :: l -> let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in - let (_, pat) = Constrintern.intern_constr_pattern Evd.empty env constr in + let (_, pat) = Constrintern.intern_constr_pattern env constr in extract_flags name tpe ((pat, b) :: subtpe) mods blacklist l | (Interface.In_Module m, b) :: l -> let path = String.concat "." m in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index db51ff6103..399471b74a 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1431,7 +1431,7 @@ open Search let interp_search_about_item = function | SearchSubPattern pat -> - let _,pat = intern_constr_pattern Evd.empty (Global.env()) pat in + let _,pat = intern_constr_pattern (Global.env()) pat in GlobSearchSubPattern pat | SearchString (s,None) when Id.is_valid s -> GlobSearchString s @@ -1448,7 +1448,7 @@ let interp_search_about_item = function let vernac_search s r = let r = interp_search_restriction r in let env = Global.env () in - let get_pattern c = snd (Constrintern.intern_constr_pattern Evd.empty env c) in + let get_pattern c = snd (Constrintern.intern_constr_pattern env c) in match s with | SearchPattern c -> msg_notice (Search.search_pattern (get_pattern c) r) |