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 /plugins | |
| 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 'plugins')
| -rw-r--r-- | plugins/syntax/number.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/syntax/number.ml b/plugins/syntax/number.ml index 89d757a72a..0e7640f430 100644 --- a/plugins/syntax/number.ml +++ b/plugins/syntax/number.ml @@ -387,10 +387,10 @@ let locate_global_inductive allow_params qid = | Globnames.TrueGlobal _ -> raise Not_found | Globnames.SynDef kn -> match Syntax_def.search_syntactic_definition kn with - | [], Notation_term.(NApp (NRef (GlobRef.IndRef i), l)) when allow_params -> + | [], Notation_term.(NApp (NRef (GlobRef.IndRef i,None), l)) when allow_params -> i, List.map (function - | Notation_term.NRef r -> Some r + | Notation_term.NRef (r,None) -> Some r | Notation_term.NHole _ -> None | _ -> raise Not_found) l | _ -> raise Not_found in |