diff options
| author | Jasper Hugunin | 2020-11-02 17:08:25 -0800 |
|---|---|---|
| committer | Jasper Hugunin | 2021-01-04 09:44:46 -0800 |
| commit | 70d557994583bd081787e28f68d627a0833eb9c0 (patch) | |
| tree | f363a0782c7395de8a0a2cf1755bd69c63faa614 /interp/notation_term.ml | |
| parent | 66e24a2365b235bd35cbba71adce30dccea60b55 (diff) | |
Remember universe instances of constants in notations
Diffstat (limited to 'interp/notation_term.ml')
| -rw-r--r-- | interp/notation_term.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/notation_term.ml b/interp/notation_term.ml index c541a19bfd..2979447cf8 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -21,7 +21,7 @@ open Glob_term type notation_constr = (* Part common to [glob_constr] and [cases_pattern] *) - | NRef of GlobRef.t + | NRef of GlobRef.t * glob_level list option | NVar of Id.t | NApp of notation_constr * notation_constr list | NHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option |