diff options
| author | Emilio Jesus Gallego Arias | 2020-02-22 13:51:55 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-22 13:51:55 -0500 |
| commit | fd67afe0f7c55799ae0a14d78f1007a0360bd552 (patch) | |
| tree | 7b77866dfda1c468eb3a0ddddd1afcd22af1a834 /interp | |
| parent | 7ef010c50c9d8efcd20d44807126efcd418c4e0d (diff) | |
| parent | 2e64c61cf64172fb0dce2d8b3996fb30e179e5ea (diff) | |
Merge PR #11635: Cleanup around the tolerability structure
Reviewed-by: ejgallego
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 *) |