diff options
| author | Hugo Herbelin | 2019-12-25 23:37:41 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-22 01:52:29 +0100 |
| commit | 8b2c4ea19c7930939c6d6d540558f042a60ac391 (patch) | |
| tree | 1892276e77bc54938fc53aa1e1a3056a5006ff79 /interp | |
| parent | b5bd769d725495d8c78c04d6721742e602a9b539 (diff) | |
Making structure of type "tolerability" and related clearer.
Also renamed it to relative_entry_level.
Correspondence between old and new representation is:
(n,L) -> LevelLt n
(n,E), (n,Prec n) -> LevelLe n
(n,Any) -> LevelSome
(n,Prec p) when n<>p was unused
Should not change global semantics (except error message in pr_arg).
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrexpr.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index 1d51109b7f..4bdacda529 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -20,8 +20,12 @@ type ident_decl = lident * universe_decl_expr option type name_decl = lname * universe_decl_expr option type notation_with_optional_scope = LastLonelyNotation | NotationInScope of string + +type entry_level = int +type entry_relative_level = LevelLt of entry_level | LevelLe of entry_level | LevelSome + type notation_entry = InConstrEntry | InCustomEntry of string -type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of string * int +type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of string * entry_level type notation_key = string (* A notation associated to a given parsing rule *) |