diff options
| author | coqbot-app[bot] | 2021-01-09 12:34:12 +0000 |
|---|---|---|
| committer | GitHub | 2021-01-09 12:34:12 +0000 |
| commit | 723440611965ccdecfd56e61c8f1f8618a08841d (patch) | |
| tree | 9d3582f11361a788c7f60568fb95d112839eec1e /interp/notation_term.ml | |
| parent | 7b946aa196490be8790cd5b46d0860b3bf6e33e1 (diff) | |
| parent | 70d557994583bd081787e28f68d627a0833eb9c0 (diff) | |
Merge PR #13299: Remember universe instances of constants in notations
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
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 |