Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adapt to Coq PR #19404: an algebra of types for the instances of notation variables #810

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Adapt to Coq PR #19404: an algebra of types for the instances of notation variables #810

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 8 additions & 2 deletions serlib/ser_constrexpr.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -165,10 +165,15 @@ type delimiter_depth = [%import: Constrexpr.delimiter_depth]
type prim_token = [%import: Constrexpr.prim_token]
[@@deriving sexp,yojson,hash,compare]

type ('a,'b,'c) notation_arg_kind = [%import: ('a,'b,'c) Constrexpr.notation_arg_kind]
[@@deriving sexp,yojson,hash,compare]

type ('a,'b,'c) notation_arg_type = [%import: ('a,'b,'c) Constrexpr.notation_arg_type]
[@@deriving sexp,yojson,hash,compare]

type cases_pattern_expr_r = [%import: Constrexpr.cases_pattern_expr_r]
and cases_pattern_expr = [%import: Constrexpr.cases_pattern_expr]
and kinded_cases_pattern_expr = [%import: Constrexpr.kinded_cases_pattern_expr]
and cases_pattern_notation_substitution = [%import: Constrexpr.cases_pattern_notation_substitution]
and constr_expr_r = [%import: Constrexpr.constr_expr_r]
and constr_expr = [%import: Constrexpr.constr_expr]
and case_expr = [%import: Constrexpr.case_expr]
Expand All @@ -178,7 +183,8 @@ and cofix_expr = [%import: Constrexpr.cofix_expr]
and fixpoint_order_expr_r = [%import: Constrexpr.fixpoint_order_expr_r]
and fixpoint_order_expr = [%import: Constrexpr.fixpoint_order_expr]
and local_binder_expr = [%import: Constrexpr.local_binder_expr]
and constr_notation_substitution = [%import: Constrexpr.constr_notation_substitution]
and notation_arg_type_expr = [%import: Constrexpr.notation_arg_type_expr]
and notation_substitution = [%import: Constrexpr.notation_substitution]
[@@deriving sexp,yojson,hash,compare]

type constr_pattern_expr = [%import: Constrexpr.constr_pattern_expr]
Expand Down
5 changes: 1 addition & 4 deletions serlib/ser_constrexpr.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -74,13 +74,10 @@ val prim_token_of_sexp : Sexp.t -> prim_token
val sexp_of_prim_token : prim_token -> Sexp.t

type cases_pattern_expr = Constrexpr.cases_pattern_expr
and cases_pattern_notation_substitution = Constrexpr.cases_pattern_notation_substitution

val cases_pattern_expr_of_sexp : Sexp.t -> cases_pattern_expr
val cases_pattern_notation_substitution_of_sexp : Sexp.t -> cases_pattern_notation_substitution

val sexp_of_cases_pattern_expr : cases_pattern_expr -> Sexp.t
val sexp_of_cases_pattern_notation_substitution : cases_pattern_notation_substitution -> Sexp.t

type instance_expr = Constrexpr.instance_expr

Expand All @@ -94,7 +91,7 @@ and fix_expr = Constrexpr.fix_expr
and cofix_expr = Constrexpr.cofix_expr
and fixpoint_order_expr = Constrexpr.fixpoint_order_expr
and local_binder_expr = Constrexpr.local_binder_expr
and constr_notation_substitution = Constrexpr.constr_notation_substitution
and notation_substitution = Constrexpr.notation_substitution
[@@deriving sexp, yojson, hash,compare]

type constr_pattern_expr = Constrexpr.constr_pattern_expr [@@deriving sexp,yojson,hash,compare]
Expand Down
4 changes: 4 additions & 0 deletions serlib/ser_genintern.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,10 @@ module Store = struct

end

type notation_variable_status =
[%import: Genintern.notation_variable_status]
[@@deriving sexp, yojson, hash, compare]

type intern_variable_status =
[%import: Genintern.intern_variable_status]
[@@deriving sexp,yojson,hash,compare]
Expand Down
3 changes: 3 additions & 0 deletions serlib/ser_genintern.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,9 @@ open Sexplib

module Store : SerType.SJHC with type t = Genintern.Store.t

type notation_variable_status = Genintern.notation_variable_status
[@@deriving sexp, yojson, hash, compare]

type intern_variable_status = Genintern.intern_variable_status
[@@deriving sexp, yojson, hash, compare]

Expand Down
Loading