From e39c84ff2dc20ce059ee6198e142ca076de8c6cb Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 19 Sep 2018 09:22:12 -0400
Subject: Fix Numeral Notations (1/4 - moving things)

Move various things from from numeral.ml to notation.ml and
notation.mli; this is required to allow the vernac command to continue
living in numeral.ml while preparing to move all of the numeral notation
interpretation logic to notation.ml

This is commit 1/4 in the fix for #8401.

This is a pure cut/paste commit, modulo adding section-heading comments.
---
 plugins/syntax/g_numeral.ml4 |  1 +
 plugins/syntax/numeral.ml    | 30 +-----------------------------
 plugins/syntax/numeral.mli   |  7 +------
 3 files changed, 3 insertions(+), 35 deletions(-)

(limited to 'plugins/syntax')

diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4
index ec14df3baa..55f61a58f9 100644
--- a/plugins/syntax/g_numeral.ml4
+++ b/plugins/syntax/g_numeral.ml4
@@ -10,6 +10,7 @@
 
 DECLARE PLUGIN "numeral_notation_plugin"
 
+open Notation
 open Numeral
 open Pp
 open Names
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index fee93593d0..7acf18da2f 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -16,6 +16,7 @@ open Globnames
 open Constrexpr
 open Constrexpr_ops
 open Constr
+open Notation
 
 (** * Numeral notation *)
 
@@ -96,10 +97,6 @@ let rec rawnum_compare s s' =
 
 (** ** Conversion between Coq [Decimal.int] and internal raw string *)
 
-type int_ty =
-  { uint : Names.inductive;
-    int : Names.inductive }
-
 (** Decimal.Nil has index 1, then Decimal.D0 has index 2 .. Decimal.D9 is 11 *)
 
 let digit_of_char c =
@@ -158,10 +155,6 @@ let rawnum_of_coqint c =
 
 (** ** Conversion between Coq [Z] and internal bigint *)
 
-type z_pos_ty =
-  { z_ty : Names.inductive;
-    pos_ty : Names.inductive }
-
 (** First, [positive] from/to bigint *)
 
 let rec pos_of_bigint posty n =
@@ -273,27 +266,6 @@ let big2raw n =
 let raw2big (n,s) =
   if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n)
 
-type target_kind =
-  | Int of int_ty (* Coq.Init.Decimal.int + uint *)
-  | UInt of Names.inductive (* Coq.Init.Decimal.uint *)
-  | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
-
-type option_kind = Option | Direct
-type conversion_kind = target_kind * option_kind
-
-type numnot_option =
-  | Nop
-  | Warning of raw_natural_number
-  | Abstract of raw_natural_number
-
-type numeral_notation_obj =
-  { to_kind : conversion_kind;
-    to_ty : GlobRef.t;
-    of_kind : conversion_kind;
-    of_ty : GlobRef.t;
-    num_ty : Libnames.qualid; (* for warnings / error messages *)
-    warning : numnot_option }
-
 let interp o ?loc n =
   begin match o.warning with
   | Warning threshold when snd n && rawnum_compare (fst n) threshold >= 0 ->
diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli
index 83ede6f48f..f96b8321f8 100644
--- a/plugins/syntax/numeral.mli
+++ b/plugins/syntax/numeral.mli
@@ -9,14 +9,9 @@
 (************************************************************************)
 
 open Libnames
-open Constrexpr
 open Vernacexpr
+open Notation
 
 (** * Numeral notation *)
 
-type numnot_option =
-  | Nop
-  | Warning of raw_natural_number
-  | Abstract of raw_natural_number
-
 val vernac_numeral_notation : locality_flag -> qualid -> qualid -> qualid -> Notation_term.scope_name -> numnot_option -> unit
-- 
cgit v1.2.3


From 4888eb7ea720eaa34af8df2769fa300f1ea37173 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 19 Sep 2018 09:32:15 -0400
Subject: Fix Numeral Notations (2/4 - exceptions, usr_err)

Switch to using exceptions rather than user errors.  This will be
required because the machinery for printing constrs is not available in
notation.ml, so we move the error message printing to himsg.ml instead.

This is commit 2/4 in the fix for #8401.
---
 plugins/syntax/numeral.ml | 32 ++++++++++++--------------------
 1 file changed, 12 insertions(+), 20 deletions(-)

(limited to 'plugins/syntax')

diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index 7acf18da2f..bc25e4730d 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -63,14 +63,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_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ".")
+      Nametab.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_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ") targets an " ++
+      Nametab.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).
@@ -224,35 +224,27 @@ let rec constr_of_glob env sigma g = match DAst.get g with
   | _ ->
       raise NotANumber
 
-let rec glob_of_constr ?loc c = match Constr.kind c with
+let rec glob_of_constr ?loc env sigma c = match Constr.kind c with
   | App (c, ca) ->
-      let c = glob_of_constr ?loc c in
-      let cel = List.map (glob_of_constr ?loc) (Array.to_list ca) in
+      let c = glob_of_constr ?loc env sigma c in
+      let cel = List.map (glob_of_constr ?loc env sigma) (Array.to_list ca) in
       DAst.make ?loc (Glob_term.GApp (c, cel))
   | Construct (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstructRef c, None))
   | Const (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstRef c, None))
   | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (IndRef ind, None))
   | Var id -> DAst.make ?loc (Glob_term.GRef (VarRef id, None))
-  | _ -> let (sigma, env) = Pfedit.get_current_context () in
-         CErrors.user_err ?loc
-           (strbrk "Unexpected term " ++
-              Printer.pr_constr_env env sigma c ++
-              strbrk " while parsing a numeral notation.")
+  | _ -> Loc.raise ?loc (NumeralNotationError(env,sigma,UnexpectedTerm c))
 
 let no_such_number ?loc ty =
   CErrors.user_err ?loc
    (str "Cannot interpret this number as a value of type " ++
     pr_qualid ty)
 
-let interp_option ty ?loc c =
+let interp_option ty ?loc env sigma c =
   match Constr.kind c with
-  | App (_Some, [| _; c |]) -> glob_of_constr ?loc c
+  | App (_Some, [| _; c |]) -> glob_of_constr ?loc env sigma c
   | App (_None, [| _ |]) -> no_such_number ?loc ty
-  | x -> let (sigma, env) = Pfedit.get_current_context () in
-         CErrors.user_err ?loc
-          (strbrk "Unexpected non-option term " ++
-             Printer.pr_constr_env env sigma c ++
-             strbrk " while parsing a numeral notation.")
+  | x -> Loc.raise ?loc (NumeralNotationError(env,sigma,UnexpectedNonOptionTerm c))
 
 let uninterp_option c =
   match Constr.kind c with
@@ -285,12 +277,12 @@ let interp o ?loc n =
   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);
-     glob_of_constr ?loc (mkApp (to_ty,[|c|]))
+     glob_of_constr ?loc env sigma (mkApp (to_ty,[|c|]))
   | _ ->
      let res = eval_constr_app env sigma to_ty c in
      match snd o.to_kind with
-     | Direct -> glob_of_constr ?loc res
-     | Option -> interp_option o.num_ty ?loc res
+     | Direct -> glob_of_constr ?loc env sigma res
+     | Option -> interp_option o.num_ty ?loc env sigma res
 
 let uninterp o (Glob_term.AnyGlobConstr n) =
   let env = Global.env () in
-- 
cgit v1.2.3


From ab0015c1c2fce185648da6c0364e6c3eb0515424 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 19 Sep 2018 09:47:16 -0400
Subject: Fix Numeral Notations (3/4 - moving more stuff)

Move most of the rest of the stuff from numeral.ml to notation.ml.  Now
that we use exceptions to print error messages, all of the
interpretation code for numeral notations can be moved to notation.ml.

This is commit 1/4 in the fix for #8401.

This is a pure cut/paste commit, modulo fixing name qualifications due
to moved things, and exposing some stuff in notation.mli (to be removed
in the next commit, where we finish the numeral notation reworking).
---
 plugins/syntax/g_numeral.ml4 |   2 +-
 plugins/syntax/numeral.ml    | 276 +------------------------------------------
 2 files changed, 2 insertions(+), 276 deletions(-)

(limited to 'plugins/syntax')

diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4
index 55f61a58f9..68b8178368 100644
--- a/plugins/syntax/g_numeral.ml4
+++ b/plugins/syntax/g_numeral.ml4
@@ -10,8 +10,8 @@
 
 DECLARE PLUGIN "numeral_notation_plugin"
 
-open Notation
 open Numeral
+open Notation
 open Pp
 open Names
 open Vernacinterp
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index bc25e4730d..1a70c9536d 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -15,56 +15,10 @@ open Libnames
 open Globnames
 open Constrexpr
 open Constrexpr_ops
-open Constr
 open Notation
 
 (** * Numeral notation *)
 
-(** Reduction
-
-    The constr [c] below isn't necessarily well-typed, since we
-    built it via an [mkApp] of a conversion function on a term
-    that starts with the right constructor but might be partially
-    applied.
-
-    At least [c] is known to be evar-free, since it comes from
-    our own ad-hoc [constr_of_glob] or from conversions such
-    as [coqint_of_rawnum].
-*)
-
-let eval_constr env sigma (c : Constr.t) =
-  let c = EConstr.of_constr c in
-  let sigma,t = Typing.type_of env sigma c in
-  let c' = Vnorm.cbv_vm env sigma c t in
-  EConstr.Unsafe.to_constr c'
-
-(* For testing with "compute" instead of "vm_compute" :
-let eval_constr env sigma (c : Constr.t) =
-  let c = EConstr.of_constr c in
-  let c' = Tacred.compute env sigma c in
-  EConstr.Unsafe.to_constr c'
-*)
-
-let eval_constr_app env sigma c1 c2 =
-  eval_constr env sigma (mkApp (c1,[| c2 |]))
-
-exception NotANumber
-
-let warn_large_num =
-  CWarnings.create ~name:"large-number" ~category:"numbers"
-    (fun ty ->
-      strbrk "Stack overflow or segmentation fault happens when " ++
-      strbrk "working with large numbers in " ++ pr_qualid ty ++
-      strbrk " (threshold may vary depending" ++
-      strbrk " on your system limits and on the command executed).")
-
-let warn_abstract_large_num =
-  CWarnings.create ~name:"abstract-large-number" ~category:"numbers"
-    (fun (ty,f) ->
-      strbrk "To avoid stack overflow, large numbers in " ++
-      pr_qualid ty ++ strbrk " are interpreted as applications of " ++
-      Nametab.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 ->
@@ -73,234 +27,6 @@ let warn_abstract_large_num_no_op =
       Nametab.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).
-    A bit nasty, but not critical: only used to decide when a
-    number is considered as large (see warnings above). *)
-
-exception Comp of int
-
-let rec rawnum_compare s s' =
- let l = String.length s and l' = String.length s' in
- if l < l' then - rawnum_compare s' s
- else
-   let d = l-l' in
-   try
-     for i = 0 to d-1 do if s.[i] != '0' then raise (Comp 1) done;
-     for i = d to l-1 do
-       let c = Pervasives.compare s.[i] s'.[i-d] in
-       if c != 0 then raise (Comp c)
-     done;
-     0
-   with Comp c -> c
-
-(***********************************************************************)
-
-(** ** Conversion between Coq [Decimal.int] and internal raw string *)
-
-(** Decimal.Nil has index 1, then Decimal.D0 has index 2 .. Decimal.D9 is 11 *)
-
-let digit_of_char c =
-  assert ('0' <= c && c <= '9');
-  Char.code c - Char.code '0' + 2
-
-let char_of_digit n =
-  assert (2<=n && n<=11);
-  Char.chr (n-2 + Char.code '0')
-
-let coquint_of_rawnum uint str =
-  let nil = mkConstruct (uint,1) in
-  let rec do_chars s i acc =
-    if i < 0 then acc
-    else
-      let dg = mkConstruct (uint, digit_of_char s.[i]) in
-      do_chars s (i-1) (mkApp(dg,[|acc|]))
-  in
-  do_chars str (String.length str - 1) nil
-
-let coqint_of_rawnum inds (str,sign) =
-  let uint = coquint_of_rawnum inds.uint str in
-  mkApp (mkConstruct (inds.int, if sign then 1 else 2), [|uint|])
-
-let rawnum_of_coquint c =
-  let rec of_uint_loop c buf =
-    match Constr.kind c with
-    | Construct ((_,1), _) (* Nil *) -> ()
-    | App (c, [|a|]) ->
-       (match Constr.kind c with
-        | Construct ((_,n), _) (* D0 to D9 *) ->
-           let () = Buffer.add_char buf (char_of_digit n) in
-           of_uint_loop a buf
-        | _ -> raise NotANumber)
-    | _ -> raise NotANumber
-  in
-  let buf = Buffer.create 64 in
-  let () = of_uint_loop c buf in
-  if Int.equal (Buffer.length buf) 0 then
-    (* To avoid ambiguities between Nil and (D0 Nil), we choose
-       to not display Nil alone as "0" *)
-    raise NotANumber
-  else Buffer.contents buf
-
-let rawnum_of_coqint c =
-  match Constr.kind c with
-  | App (c,[|c'|]) ->
-     (match Constr.kind c with
-      | Construct ((_,1), _) (* Pos *) -> (rawnum_of_coquint c', true)
-      | Construct ((_,2), _) (* Neg *) -> (rawnum_of_coquint c', false)
-      | _ -> raise NotANumber)
-  | _ -> raise NotANumber
-
-
-(***********************************************************************)
-
-(** ** Conversion between Coq [Z] and internal bigint *)
-
-(** First, [positive] from/to bigint *)
-
-let rec pos_of_bigint posty n =
-  match Bigint.div2_with_rest n with
-  | (q, false) ->
-      let c = mkConstruct (posty, 2) in (* xO *)
-      mkApp (c, [| pos_of_bigint posty q |])
-  | (q, true) when not (Bigint.equal q Bigint.zero) ->
-      let c = mkConstruct (posty, 1) in (* xI *)
-      mkApp (c, [| pos_of_bigint posty q |])
-  | (q, true) ->
-      mkConstruct (posty, 3) (* xH *)
-
-let rec bigint_of_pos c = match Constr.kind c with
-  | Construct ((_, 3), _) -> (* xH *) Bigint.one
-  | App (c, [| d |]) ->
-      begin match Constr.kind c with
-      | Construct ((_, n), _) ->
-          begin match n with
-          | 1 -> (* xI *) Bigint.add_1 (Bigint.mult_2 (bigint_of_pos d))
-          | 2 -> (* xO *) Bigint.mult_2 (bigint_of_pos d)
-          | n -> assert false (* no other constructor of type positive *)
-          end
-      | x -> raise NotANumber
-      end
-  | x -> raise NotANumber
-
-(** Now, [Z] from/to bigint *)
-
-let z_of_bigint { z_ty; pos_ty } n =
-  if Bigint.equal n Bigint.zero then
-    mkConstruct (z_ty, 1) (* Z0 *)
-  else
-    let (s, n) =
-      if Bigint.is_pos_or_zero n then (2, n) (* Zpos *)
-      else (3, Bigint.neg n) (* Zneg *)
-    in
-    let c = mkConstruct (z_ty, s) in
-    mkApp (c, [| pos_of_bigint pos_ty n |])
-
-let bigint_of_z z = match Constr.kind z with
-  | Construct ((_, 1), _) -> (* Z0 *) Bigint.zero
-  | App (c, [| d |]) ->
-      begin match Constr.kind c with
-      | Construct ((_, n), _) ->
-          begin match n with
-          | 2 -> (* Zpos *) bigint_of_pos d
-          | 3 -> (* Zneg *) Bigint.neg (bigint_of_pos d)
-          | n -> assert false (* no other constructor of type Z *)
-          end
-      | _ -> raise NotANumber
-      end
-  | _ -> raise NotANumber
-
-(** The uninterp function below work at the level of [glob_constr]
-    which is too low for us here. So here's a crude conversion back
-    to [constr] for the subset that concerns us. *)
-
-let rec constr_of_glob env sigma g = match DAst.get g with
-  | Glob_term.GRef (ConstructRef c, _) ->
-      let sigma,c = Evd.fresh_constructor_instance env sigma c in
-      sigma,mkConstructU c
-  | Glob_term.GApp (gc, gcl) ->
-      let sigma,c = constr_of_glob env sigma gc in
-      let sigma,cl = List.fold_left_map (constr_of_glob env) sigma gcl in
-      sigma,mkApp (c, Array.of_list cl)
-  | _ ->
-      raise NotANumber
-
-let rec glob_of_constr ?loc env sigma c = match Constr.kind c with
-  | App (c, ca) ->
-      let c = glob_of_constr ?loc env sigma c in
-      let cel = List.map (glob_of_constr ?loc env sigma) (Array.to_list ca) in
-      DAst.make ?loc (Glob_term.GApp (c, cel))
-  | Construct (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstructRef c, None))
-  | Const (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstRef c, None))
-  | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (IndRef ind, None))
-  | Var id -> DAst.make ?loc (Glob_term.GRef (VarRef id, None))
-  | _ -> Loc.raise ?loc (NumeralNotationError(env,sigma,UnexpectedTerm c))
-
-let no_such_number ?loc ty =
-  CErrors.user_err ?loc
-   (str "Cannot interpret this number as a value of type " ++
-    pr_qualid ty)
-
-let interp_option ty ?loc env sigma c =
-  match Constr.kind c with
-  | App (_Some, [| _; c |]) -> glob_of_constr ?loc env sigma c
-  | App (_None, [| _ |]) -> no_such_number ?loc ty
-  | x -> Loc.raise ?loc (NumeralNotationError(env,sigma,UnexpectedNonOptionTerm c))
-
-let uninterp_option c =
-  match Constr.kind c with
-  | App (_Some, [| _; x |]) -> x
-  | _ -> raise NotANumber
-
-let big2raw n =
-  if Bigint.is_pos_or_zero n then (Bigint.to_string n, true)
-  else (Bigint.to_string (Bigint.neg n), false)
-
-let raw2big (n,s) =
-  if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n)
-
-let interp o ?loc n =
-  begin match o.warning with
-  | Warning threshold when snd n && rawnum_compare (fst n) threshold >= 0 ->
-     warn_large_num o.num_ty
-  | _ -> ()
-  end;
-  let c = match fst o.to_kind with
-    | Int int_ty -> coqint_of_rawnum int_ty n
-    | UInt uint_ty when snd n -> coquint_of_rawnum uint_ty (fst n)
-    | UInt _ (* n <= 0 *) -> no_such_number ?loc o.num_ty
-    | Z z_pos_ty -> z_of_bigint z_pos_ty (raw2big n)
-  in
-  let env = Global.env () in
-  let sigma = Evd.from_env env 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);
-     glob_of_constr ?loc env sigma (mkApp (to_ty,[|c|]))
-  | _ ->
-     let res = eval_constr_app env sigma to_ty c in
-     match snd o.to_kind with
-     | Direct -> glob_of_constr ?loc env sigma res
-     | Option -> interp_option o.num_ty ?loc env sigma res
-
-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_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
-    let c = if snd o.of_kind == Direct then c else uninterp_option c in
-    match fst o.of_kind with
-    | Int _ -> Some (rawnum_of_coqint c)
-    | UInt _ -> Some (rawnum_of_coquint c, true)
-    | Z _ -> Some (big2raw (bigint_of_z c))
-  with
-  | Type_errors.TypeError _ | Pretype_errors.PretypeError _ -> None (* cf. eval_constr_app *)
-  | NotANumber -> None (* all other functions except big2raw *)
-
 (* Here we only register the interp and uninterp functions
    for a particular Numeral Notation (determined by a unique
    string). The actual activation of the notation will be done
@@ -310,7 +36,7 @@ let uninterp o (Glob_term.AnyGlobConstr n) =
 
 let load_numeral_notation _ (_, (uid,opts)) =
   Notation.register_rawnumeral_interpretation
-    ~allow_overwrite:true uid (interp opts, uninterp opts)
+    ~allow_overwrite:true uid (Notation.Numeral.interp opts, Notation.Numeral.uninterp opts)
 
 let cache_numeral_notation x = load_numeral_notation 1 x
 
-- 
cgit v1.2.3


From 87de52b9b4fd793ee9ddd231633513b6c5070e19 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 19 Sep 2018 09:52:04 -0400
Subject: Fix Numeral Notations (4/4 - fixing synch)

This fixes #8401
Supersedes / closes #8407

Vernacular-command-registered numeral notations now live in the summary,
and the interpretation function for them is hard-coded.

Plugin-registered numeral notations are still unsynchronized, and only
the UIDs of these functions gets synchronized.  I am not 100% sure why
this is fine, but the test-suite file working suggests that it is fine.
I think it is because worker delegation correctly handles
non-synchronized state which is declared at `Declare ML Module`-time.

This final commit changes the synchronization of numeral notations (and
deletes no-longer-used declarations in notation.mli that were introduced
temporarily in the last commit).  Since the interpretation can now be
done in notation.ml, we no longer need to register unique ids for
numeral notation (un)interp functions, and can instead synchronize the
underlying constants with the document state.  This is the change that
actually fixes #8401.
---
 plugins/syntax/ascii_syntax.ml  |  2 +-
 plugins/syntax/g_numeral.ml4    |  2 +-
 plugins/syntax/int31_syntax.ml  |  2 +-
 plugins/syntax/numeral.ml       | 34 ++++------------------------------
 plugins/syntax/r_syntax.ml      |  2 +-
 plugins/syntax/string_syntax.ml |  2 +-
 6 files changed, 9 insertions(+), 35 deletions(-)

(limited to 'plugins/syntax')

diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 5e36fbeb81..53153198f9 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -94,7 +94,7 @@ let _ =
   at_declare_ml_module enable_prim_token_interpretation
     { pt_local = false;
       pt_scope = sc;
-      pt_uid = sc;
+      pt_interp_info = Uid sc;
       pt_required = (ascii_path,ascii_module);
       pt_refs = [static_glob_Ascii];
       pt_in_match = true }
diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4
index 68b8178368..55f61a58f9 100644
--- a/plugins/syntax/g_numeral.ml4
+++ b/plugins/syntax/g_numeral.ml4
@@ -10,8 +10,8 @@
 
 DECLARE PLUGIN "numeral_notation_plugin"
 
-open Numeral
 open Notation
+open Numeral
 open Pp
 open Names
 open Vernacinterp
diff --git a/plugins/syntax/int31_syntax.ml b/plugins/syntax/int31_syntax.ml
index d3ffe936a9..e34a401c2c 100644
--- a/plugins/syntax/int31_syntax.ml
+++ b/plugins/syntax/int31_syntax.ml
@@ -108,7 +108,7 @@ let _ =
   at_declare_ml_module enable_prim_token_interpretation
     { pt_local = false;
       pt_scope = int31_scope;
-      pt_uid = int31_scope;
+      pt_interp_info = Uid int31_scope;
       pt_required = (int31_path,int31_module);
       pt_refs = [int31_construct];
       pt_in_match = true }
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index 1a70c9536d..10a0af0b8f 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -27,29 +27,6 @@ let warn_abstract_large_num_no_op =
       Nametab.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ") targets an " ++
       strbrk "option type.")
 
-(* Here we only register the interp and uninterp functions
-   for a particular Numeral Notation (determined by a unique
-   string). The actual activation of the notation will be done
-   later (cf. Notation.enable_prim_token_interpretation).
-   This registration of interp/uninterp must be added in the
-   libstack, otherwise this won't work through a Require. *)
-
-let load_numeral_notation _ (_, (uid,opts)) =
-  Notation.register_rawnumeral_interpretation
-    ~allow_overwrite:true uid (Notation.Numeral.interp opts, Notation.Numeral.uninterp opts)
-
-let cache_numeral_notation x = load_numeral_notation 1 x
-
-(* TODO: substitution ?
-   TODO: uid pas stable par substitution dans opts
- *)
-
-let inNumeralNotation : string * numeral_notation_obj -> Libobject.obj =
-  Libobject.declare_object {
-    (Libobject.default_object "NUMERAL NOTATION") with
-    Libobject.cache_function = cache_numeral_notation;
-    Libobject.load_function = load_numeral_notation }
-
 let get_constructors ind =
   let mib,oib = Global.lookup_inductive ind in
   let mc = oib.Declarations.mind_consnames in
@@ -154,15 +131,12 @@ let vernac_numeral_notation local ty f g scope opts =
   (match opts, to_kind with
    | Abstract _, (_, Option) -> warn_abstract_large_num_no_op o.to_ty
    | _ -> ());
-  (* TODO: un hash suffit-il ? *)
-  let uid = Marshal.to_string o [] in
-  let i = Notation.(
+  let i =
        { pt_local = local;
          pt_scope = scope;
-         pt_uid = uid;
+         pt_interp_info = NumeralNotation o;
          pt_required = Nametab.path_of_global (IndRef tyc),[];
          pt_refs = constructors;
-         pt_in_match = true })
+         pt_in_match = true }
   in
-  Lib.add_anonymous_leaf (inNumeralNotation (uid,o));
-  Notation.enable_prim_token_interpretation i
+  enable_prim_token_interpretation i
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 04946c158b..49497aef54 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -143,7 +143,7 @@ let _ =
   at_declare_ml_module enable_prim_token_interpretation
     { pt_local = false;
       pt_scope = r_scope;
-      pt_uid = r_scope;
+      pt_interp_info = Uid r_scope;
       pt_required = (r_path,["Coq";"Reals";"Rdefinitions"]);
       pt_refs = [glob_IZR];
       pt_in_match = false }
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index 640bcfde91..7478c1e978 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -75,7 +75,7 @@ let _ =
   at_declare_ml_module enable_prim_token_interpretation
     { pt_local = false;
       pt_scope = sc;
-      pt_uid = sc;
+      pt_interp_info = Uid sc;
       pt_required = (string_path,["Coq";"Strings";"String"]);
       pt_refs = [static_glob_String; static_glob_EmptyString];
       pt_in_match = true }
-- 
cgit v1.2.3