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 /plugins/syntax/number.ml | |
| parent | 66e24a2365b235bd35cbba71adce30dccea60b55 (diff) | |
Remember universe instances of constants in notations
Diffstat (limited to 'plugins/syntax/number.ml')
| -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 |