From 70d557994583bd081787e28f68d627a0833eb9c0 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Mon, 2 Nov 2020 17:08:25 -0800
Subject: Remember universe instances of constants in notations

---
 interp/constrintern.mli | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'interp/constrintern.mli')

diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index f92a54e23f..65b63962d0 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -150,6 +150,10 @@ val interp_constr_pattern :
 (** Raise Not_found if syndef not bound to a name and error if unexisting ref *)
 val intern_reference : qualid -> GlobRef.t
 
+(** For syntactic definitions: check if abbreviation to a name
+    and avoid early insertion of maximal implicit arguments *)
+val try_interp_name_alias : 'a list * constr_expr -> notation_constr
+
 (** Expands abbreviations (syndef); raise an error if not existing *)
 val interp_reference : ltac_sign -> qualid -> glob_constr
 
-- 
cgit v1.2.3