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 /vernac | |
| parent | 66e24a2365b235bd35cbba71adce30dccea60b55 (diff) | |
Remember universe instances of constants in notations
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/metasyntax.ml | 8 | ||||
| -rw-r--r-- | vernac/prettyp.ml | 2 |
2 files changed, 2 insertions, 8 deletions
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index e6244ee3b5..2fe402ff08 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1793,15 +1793,9 @@ let remove_delimiters local scope = let add_class_scope local scope cl = Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeClasses cl)) -(* Check if abbreviation to a name and avoid early insertion of - maximal implicit arguments *) -let try_interp_name_alias = function - | [], { CAst.v = CRef (ref,_) } -> intern_reference ref - | _ -> raise Not_found - let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing } = let acvars,pat,reversibility = - try Id.Map.empty, NRef (try_interp_name_alias (vars,c)), APrioriReversible + try Id.Map.empty, try_interp_name_alias (vars,c), APrioriReversible with Not_found -> let fold accu id = Id.Map.add id NtnInternTypeAny accu in let i_vars = List.fold_left fold Id.Map.empty vars in diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 0fc6c7f87b..79a0cdf8d1 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -947,7 +947,7 @@ let print_about_any ?loc env sigma k udecl = [hov 0 (str "Expands to: " ++ pr_located_qualid k)]) | Syntactic kn -> let () = match Syntax_def.search_syntactic_definition kn with - | [],Notation_term.NRef ref -> Dumpglob.add_glob ?loc ref + | [],Notation_term.NRef (ref,_) -> Dumpglob.add_glob ?loc ref | _ -> () in v 0 ( print_syntactic_def env kn ++ fnl () ++ |