diff options
| author | Enrico Tassi | 2021-03-19 12:27:14 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2021-04-07 19:59:46 +0200 |
| commit | b47931125432df88171c7e8a879294508a603aa9 (patch) | |
| tree | 64dca669a00da9d64f1ad687e9f18c65b69ec3c0 /vernac/metasyntax.ml | |
| parent | 59d0462f35818c12a0727a560d7b9ecf2ceea994 (diff) | |
cleanup: less exceptions, removal of try_interp_name_alias
Diffstat (limited to 'vernac/metasyntax.ml')
| -rw-r--r-- | vernac/metasyntax.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index f9f65a8c30..692f1d7388 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1795,8 +1795,10 @@ let add_class_scope local scope cl = let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing } = let acvars,pat,reversibility = - try Id.Map.empty, try_interp_name_alias (vars,c), APrioriReversible - with Not_found -> + match vars, intern_name_alias c with + | [], Some(r,u) -> + Id.Map.empty, NRef(r, u), APrioriReversible + | _ -> let fold accu id = Id.Map.add id NtnInternTypeAny accu in let i_vars = List.fold_left fold Id.Map.empty vars in let nenv = { |