diff options
| author | Emilio Jesus Gallego Arias | 2020-02-19 15:56:50 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-19 15:56:50 -0500 |
| commit | a644482acd84427db0e64450c3fc41ad321e83cd (patch) | |
| tree | bac186931ae4170d1f1b0e3c043be95ebbc8e243 /interp/notation.mli | |
| parent | 2b72b403d82c15d0420603142e14ab50c7e590c1 (diff) | |
| parent | 25cab58df1171c9419396342e9ecc3094b74eca5 (diff) | |
Merge PR #11636: Revert buggy commit mistakenly pushed with #11530
Reviewed-by: ejgallego
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index 707be6cb87..ea5125f7ec 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -305,12 +305,9 @@ val availability_of_entry_coercion : notation_entry_level -> notation_entry_leve val declare_custom_entry_has_global : string -> int -> unit val declare_custom_entry_has_ident : string -> int -> unit -val declare_custom_entry_has_numeral : string -> int -> unit -val declare_custom_entry_has_string : string -> int -> unit val entry_has_global : notation_entry_level -> bool val entry_has_ident : notation_entry_level -> bool -val entry_has_prim_token : prim_token -> notation_entry_level -> bool (** Rem: printing rules for primitive token are canonical *) |