simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-09 20:55:39 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Add simple fonctor for dot backend

Browse source
This commit is contained in:
Guillaume Bury 2017-02-18 15:16:53 +01:00
parent 7776b6e2f0
commit 9019de5a95
2 changed files with 9 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/backend/dot.ml
View file

@ -101,5 +101,9 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom and type lemma := S.lemm
end end
module Simple(S : Res.S)(A : Arg with type atom := S.St.formula and type lemma := S.lemma) =
Make(S)(struct
let lemma_info = A.lemma_info
let print_atom fmt a = A.print_atom fmt a.S.St.lit
end)

4
src/backend/dot.mli
View file

@ -48,3 +48,7 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom and type lemma := S.lemm
S with type t := S.proof S with type t := S.proof
(** Functor for making a module to export proofs to the DOT format. *) (** Functor for making a module to export proofs to the DOT format. *)
module Simple(S : Res.S)(A : Arg with type atom := S.St.formula and type lemma := S.lemma) :
S with type t := S.proof
(** Functor for making a module to export proofs to the DOT format. *)