diff options
| author | Hugo Herbelin | 2018-06-29 12:13:00 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-07-29 02:40:22 +0200 |
| commit | a90aa1a2d7f0fd12621e744a67cc8c2abd24f9f8 (patch) | |
| tree | fdbfbc726e8652cf7524685cb1d24b5f5df71464 /vernac/egramcoq.ml | |
| parent | bc480bb7068b0ffeeb8ad5cb90ee73fabc068d5f (diff) | |
Supporting locality flag for custom entries + compatibility with modules.
Also prevents to use an entry name already defined.
Diffstat (limited to 'vernac/egramcoq.ml')
| -rw-r--r-- | vernac/egramcoq.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 65e5f4bede..720f9b774a 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -255,7 +255,7 @@ let interp_constr_entry_key : type r. _ -> r target -> int -> r Entry.t * int op fun custom forpat level -> match custom with | InCustomEntry s -> - (let (entry_for_constr, entry_for_patttern) = find_custom_entries s in + (let (entry_for_constr, entry_for_patttern) = find_custom_entry s in match forpat with | ForConstr -> entry_for_constr, Some level | ForPattern -> entry_for_patttern, Some level) @@ -272,7 +272,7 @@ let target_entry : type s. notation_entry -> s target -> s Entry.t = function | ForConstr -> Constr.operconstr | ForPattern -> Constr.pattern) | InCustomEntry s -> - let (entry_for_constr, entry_for_patttern) = find_custom_entries s in + let (entry_for_constr, entry_for_patttern) = find_custom_entry s in function | ForConstr -> entry_for_constr | ForPattern -> entry_for_patttern |