Skip to content

Commit bad6797

Browse files
authored
Merge pull request #996 from SkySkimmer/split-nota
Adapt to rocq-prover/rocq#20926 (notations code movement)
2 parents 9d94cae + 6321aab commit bad6797

File tree

5 files changed

+5
-5
lines changed

5 files changed

+5
-5
lines changed

serlib/plugins/syntax/ser_g_number_syntax.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ open Ppx_compare_lib.Builtin
1313
open Ppx_hash_lib.Std.Hash.Builtin
1414

1515
module Libnames = Ser_libnames
16-
module Notation = Ser_notation
16+
module PrimNotations = Ser_primNotations
1717

1818
module A2 = struct
1919
type t = Ser_number_string.number_option

serlib/plugins/syntax/ser_number_string.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ open Ppx_hash_lib.Std.Hash.Builtin
1111
open Ppx_compare_lib.Builtin
1212

1313
module Libnames = Serlib.Ser_libnames
14-
module Notation = Serlib.Ser_notation
14+
module PrimNotations = Serlib.Ser_primNotations
1515

1616
type number_string_via =
1717
[%import: Number_string_notation_plugin.Number_string.number_string_via]

serlib/ser_notation_gram.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ module Constrexpr = Ser_constrexpr
2323
module Tok = Ser_tok
2424
module Extend = Ser_extend
2525
module Gramlib = Ser_gramlib
26-
module Notation = Ser_notation
26+
module PrimNotations = Ser_primNotations
2727
module Notationextern = Ser_notationextern
2828

2929
(* type precedence =

serlib/ser_notation.ml renamed to serlib/ser_primNotations.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,6 @@ module NumTok = Ser_numTok
2020
module Constrexpr = Ser_constrexpr
2121

2222
type numnot_option =
23-
[%import: Notation.numnot_option]
23+
[%import: PrimNotations.numnot_option]
2424
[@@deriving sexp,yojson,hash,compare]
2525

serlib/ser_notation.mli renamed to serlib/ser_primNotations.mli

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,4 +16,4 @@
1616
(* Written by: Emilio J. Gallego Arias and others *)
1717
(************************************************************************)
1818

19-
type numnot_option = Notation.numnot_option [@@deriving sexp,yojson,hash,compare]
19+
type numnot_option = PrimNotations.numnot_option [@@deriving sexp,yojson,hash,compare]

0 commit comments

Comments
 (0)