Add Numeral Notation GlobRef printing/parsing

Now we support using inductive constructors and section-local variables
as numeral notation printing and parsing functions.

I'm not sure that I got the econstr conversion right.

2 files changed, 46 insertions, 26 deletions

diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index 8dced1a8de..6f657fc3a5 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -62,14 +62,14 @@ let warn_abstract_large_num =
     (fun (ty,f) ->
       strbrk "To avoid stack overflow, large numbers in " ++
       pr_qualid ty ++ strbrk " are interpreted as applications of " ++
-      Printer.pr_constant (Global.env ()) f ++ strbrk ".")
+      Printer.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ".")
 
 let warn_abstract_large_num_no_op =
   CWarnings.create ~name:"abstract-large-number-no-op" ~category:"numbers"
     (fun f ->
       strbrk "The 'abstract after' directive has no effect when " ++
       strbrk "the parsing function (" ++
-      Printer.pr_constant (Global.env ()) f ++ strbrk ") targets an " ++
+      Printer.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ") targets an " ++
       strbrk "option type.")
 
 (** Comparing two raw numbers (base 10, big-endian, non-negative).
@@ -288,9 +288,9 @@ type numnot_option =
 
 type numeral_notation_obj =
   { to_kind : conversion_kind;
-    to_ty : Constant.t;
+    to_ty : GlobRef.t;
     of_kind : conversion_kind;
-    of_ty : Constant.t;
+    of_ty : GlobRef.t;
     num_ty : Libnames.qualid; (* for warnings / error messages *)
     warning : numnot_option }
 
@@ -308,8 +308,8 @@ let interp o ?loc n =
   in
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  let sigma,to_ty = Evd.fresh_constant_instance env sigma o.to_ty in
-  let to_ty = mkConstU to_ty in
+  let sigma,to_ty = Evd.fresh_global env sigma o.to_ty in
+  let to_ty = EConstr.Unsafe.to_constr to_ty in
   match o.warning, snd o.to_kind with
   | Abstract threshold, Direct when rawnum_compare (fst n) threshold >= 0 ->
      warn_abstract_large_num (o.num_ty,o.to_ty);
@@ -323,8 +323,8 @@ let interp o ?loc n =
 let uninterp o (Glob_term.AnyGlobConstr n) =
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  let sigma,of_ty = Evd.fresh_constant_instance env sigma o.of_ty in
-  let of_ty = mkConstU of_ty in
+  let sigma,of_ty = Evd.fresh_global env sigma o.of_ty in
+  let of_ty = EConstr.Unsafe.to_constr of_ty in
   try
     let sigma,n = constr_of_glob env sigma n in
     let c = eval_constr_app env sigma of_ty n in
@@ -395,10 +395,6 @@ let locate_globref q =
   try Nametab.locate q
   with Not_found -> Nametab.error_global_not_found q
 
-let locate_constant q =
-  try Nametab.locate_constant 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
@@ -423,8 +419,8 @@ 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_constant f in
-  let of_ty = locate_constant g in
+  let to_ty = locate_globref f in
+  let of_ty = locate_globref g in
   let cty = mkRefC ty in
   let app x y = mkAppC (x,[y]) in
   let cref q = mkRefC q in
diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v
index 2072fbbf62..e63b9dc4c7 100644
--- a/test-suite/success/NumeralNotations.v
+++ b/test-suite/success/NumeralNotations.v
@@ -123,42 +123,52 @@ End Test6_2.
 
 Module Test7.
   Local Set Primitive Projections.
-  Record > wuint := wrap { unwrap : Decimal.uint }.
+  Record wuint := wrap { unwrap : Decimal.uint }.
   Delimit Scope wuint_scope with wuint.
-  Fail Numeral Notation wuint wrap unwrap : wuint_scope.
+  Numeral Notation wuint wrap unwrap : wuint_scope.
+  Check let v := 0%wuint in v : wuint.
+  Check let v := 1%wuint in v : wuint.
 End Test7.
 
 Module Test8.
   Local Set Primitive Projections.
-  Record > wuint := wrap { unwrap : Decimal.uint }.
-  Delimit Scope wuint_scope with wuint.
+  Record wuint := wrap { unwrap : Decimal.uint }.
+  Delimit Scope wuint8_scope with wuint8.
+  Delimit Scope wuint8'_scope with wuint8'.
   Section with_var.
     Context (dummy : unit).
     Definition wrap' := let __ := dummy in wrap.
     Definition unwrap' := let __ := dummy in unwrap.
-    Global Numeral Notation wuint wrap' unwrap' : wuint_scope.
-    Check let v := 0%wuint in v : wuint.
+    Global Numeral Notation wuint wrap' unwrap' : wuint8_scope.
+    Check let v := 0%wuint8 in v : wuint.
   End with_var.
-  Fail Check let v := 0%wuint in v : wuint.
+  Check let v := 0%wuint8 in v : nat.
+  Fail Check let v := 0%wuint8 in v : wuint.
   Compute wrap (Nat.to_uint 0).
 
   Notation wrap'' := wrap.
   Notation unwrap'' := unwrap.
-  Fail Numeral Notation wuint wrap'' unwrap'' : wuint_scope.
+  Fail Numeral Notation wuint wrap'' unwrap'' : wuint8'_scope.
+  Fail Check let v := 0%wuint8' in v : wuint.
 End Test8.
 
 Module Test9.
+  Delimit Scope wuint9_scope with wuint9.
+  Delimit Scope wuint9'_scope with wuint9'.
   Section with_let.
     Local Set Primitive Projections.
-    Record > wuint := wrap { unwrap : Decimal.uint }.
+    Record wuint := wrap { unwrap : Decimal.uint }.
     Let wrap' := wrap.
     Let unwrap' := unwrap.
     Local Notation wrap'' := wrap.
     Local Notation unwrap'' := unwrap.
-    Delimit Scope wuint_scope with wuint.
-    Fail Numeral Notation wuint wrap' unwrap' : wuint_scope.
-    Fail Numeral Notation wuint wrap'' unwrap'' : wuint_scope.
+    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.
   End with_let.
+  Check let v := 0%wuint9 in v : nat.
+  Fail Check let v := 0%wuint9 in v : wuint.
 End Test9.
 
 Module Test10.
@@ -175,3 +185,17 @@ Module Test10.
   (* Check that there is no warning here *)
   Numeral Notation unit of_any_uint to_uint : unit2_scope (abstract after 1).
 End Test10.
+
+Module Test11.
+  (* Test that numeral notations don't work on proof-local variables, especially not ones containing evars *)
+  Inductive unit11 := tt11.
+  Delimit Scope unit11_scope with unit11.
+  Goal True.
+    evar (to_uint : unit11 -> Decimal.uint).
+    evar (of_uint : Decimal.uint -> unit11).
+    Fail Numeral Notation unit11 of_uint to_uint : uint11_scope.
+    exact I.
+    Unshelve.
+    all: solve [ constructor ].
+  Qed.
+End Test11.