diff options
| author | Pierre-Marie Pédrot | 2013-12-17 15:08:06 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2013-12-17 15:13:22 +0100 |
| commit | 16677f3d4e71b2f971ed36bbbc3b95d8908a1b13 (patch) | |
| tree | d70ab7e108af307cbd9e996b78e0f9f5e945aa42 /toplevel | |
| parent | fb59652405d0e6a9d1100142d473374cd82ae16b (diff) | |
Removing the need of evarmaps in constr internalization.
Actually, this was wrong, as evars should not appear until interpretation.
Evarmaps were only passed around uselessly, and often fed with dummy or
irrelevant values.
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) |