[numeral notations] support aliases

Aliases of global references can now be used in numeral notations

3 files changed, 44 insertions, 22 deletions

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 6f655340da..886ca0472a 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1474,9 +1474,13 @@ Numeral notations
 
   .. exn:: The reference @ident was not found in the current environment.
 
+    Identifiers passed to :cmd:`Numeral Notation` must exist in the
+    global environment.
+
+  .. exn:: @ident is bound to a notation that does not denote a reference.
+
     Identifiers passed to :cmd:`Numeral Notation` must be global
-    definitions, not notations, section variables, section-local
-    :g:`Let` bound identifiers, etc.
+    references, or notations which denote to single identifiers.
 
   .. warn:: Stack overflow or segmentation fault happens when working with large numbers in @type (threshold may vary depending on your system limits and on the command executed).
 
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index 6f657fc3a5..321992eda6 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -391,10 +391,6 @@ let locate_int () =
   { uint = locate_ind q_uint;
     int = locate_ind q_int }
 
-let locate_globref q =
-  try Nametab.locate q
-  with Not_found -> Nametab.error_global_not_found q
-
 let has_type f ty =
   let (sigma, env) = Pfedit.get_current_context () in
   let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in
@@ -418,9 +414,9 @@ let type_error_of g ty loadZ =
 let vernac_numeral_notation ty f g scope opts =
   let int_ty = locate_int () in
   let z_pos_ty = locate_z () in
-  let tyc = locate_globref ty in
-  let to_ty = locate_globref f in
-  let of_ty = locate_globref g in
+  let tyc = Smartlocate.global_inductive_with_alias ty in
+  let to_ty = Smartlocate.global_with_alias f in
+  let of_ty = Smartlocate.global_with_alias g in
   let cty = mkRefC ty in
   let app x y = mkAppC (x,[y]) in
   let cref q = mkRefC q in
@@ -432,14 +428,7 @@ let vernac_numeral_notation ty f g scope opts =
   let cuint = cref q_uint in
   let coption = cref q_option in
   let opt r = app coption r in
-  (* Check that [ty] is an inductive type *)
-  let constructors = match tyc with
-    | IndRef ind ->
-       get_constructors ind
-    | ConstRef _ | ConstructRef _ | VarRef _ ->
-       CErrors.user_err
-        (pr_qualid ty ++ str " is not an inductive type.")
-  in
+  let constructors = get_constructors tyc in
   (* Check the type of f *)
   let to_kind =
     if has_type f (arrow cint cty) then Int int_ty, Direct
@@ -480,7 +469,7 @@ let vernac_numeral_notation ty f g scope opts =
   let i = Notation.(
        { pt_scope = scope;
          pt_uid = uid;
-         pt_required = Nametab.path_of_global tyc,[];
+         pt_required = Nametab.path_of_global (IndRef tyc),[];
          pt_refs = constructors;
          pt_in_match = true })
   in
diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v
index e63b9dc4c7..5a58a1b72d 100644
--- a/test-suite/success/NumeralNotations.v
+++ b/test-suite/success/NumeralNotations.v
@@ -148,8 +148,8 @@ Module Test8.
 
   Notation wrap'' := wrap.
   Notation unwrap'' := unwrap.
-  Fail Numeral Notation wuint wrap'' unwrap'' : wuint8'_scope.
-  Fail Check let v := 0%wuint8' in v : wuint.
+  Numeral Notation wuint wrap'' unwrap'' : wuint8'_scope.
+  Check let v := 0%wuint8' in v : wuint.
 End Test8.
 
 Module Test9.
@@ -164,8 +164,8 @@ Module Test9.
     Local Notation unwrap'' := unwrap.
     Numeral Notation wuint wrap' unwrap' : wuint9_scope.
     Check let v := 0%wuint9 in v : wuint.
-    Fail Numeral Notation wuint wrap'' unwrap'' : wuint9'_scope.
-    Fail Check let v := 0%wuint9' in v : wuint.
+    Numeral Notation wuint wrap'' unwrap'' : wuint9'_scope.
+    Check let v := 0%wuint9' in v : wuint.
   End with_let.
   Check let v := 0%wuint9 in v : nat.
   Fail Check let v := 0%wuint9 in v : wuint.
@@ -199,3 +199,32 @@ Module Test11.
     all: solve [ constructor ].
   Qed.
 End Test11.
+
+Module Test12.
+  (* Test for numeral notations on context variables *)
+  Delimit Scope test12_scope with test12.
+  Section test12.
+    Context (to_uint : unit -> Decimal.uint) (of_uint : Decimal.uint -> unit).
+
+    Numeral Notation unit of_uint to_uint : test12_scope.
+    Check let v := 1%test12 in v : unit.
+  End test12.
+End Test12.
+
+Module Test13.
+  (* Test for numeral notations on notations which do not denote references *)
+  Delimit Scope test13_scope with test13.
+  Delimit Scope test13'_scope with test13'.
+  Delimit Scope test13''_scope with test13''.
+  Definition to_uint (x y : unit) : Decimal.uint := Nat.to_uint O.
+  Definition of_uint (x : Decimal.uint) : unit := tt.
+  Definition to_uint_good := to_uint tt.
+  Notation to_uint' := (to_uint tt).
+  Notation to_uint'' := (to_uint _).
+  Numeral Notation unit of_uint to_uint_good : test13_scope.
+  Check let v := 0%test13 in v : unit.
+  Fail Numeral Notation unit of_uint to_uint' : test13'_scope.
+  Fail Check let v := 0%test13' in v : unit.
+  Fail Numeral Notation unit of_uint to_uint'' : test13''_scope.
+  Fail Check let v := 0%test13'' in v : unit.
+End Test13.