mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 11:15:43 -05:00
Better syntax for functor signature in solver_types
This commit is contained in:
parent
1a0fc95147
commit
fd4d52b7a6
1 changed files with 2 additions and 6 deletions
|
|
@ -13,15 +13,11 @@
|
|||
|
||||
module type S = Solver_types_intf.S
|
||||
|
||||
module McMake :
|
||||
functor (E : Expr_intf.S) ->
|
||||
functor (Dummy : sig end) ->
|
||||
module McMake (E : Expr_intf.S)(Dummy : sig end):
|
||||
S with type term = E.Term.t and type formula = E.Formula.t and type proof = E.proof
|
||||
(** Functor to instantiate the types of clauses for a solver. *)
|
||||
|
||||
module SatMake :
|
||||
functor (E : Formula_intf.S) ->
|
||||
functor (Dummy : sig end) ->
|
||||
module SatMake (E : Formula_intf.S)(Dummy : sig end):
|
||||
S with type term = E.t and type formula = E.t and type proof = E.proof
|
||||
(** Functor to instantiate the types of clauses for a solver. *)
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue