From 9019de5a952d772075d06f6adcb409ffb4e12670 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Sat, 18 Feb 2017 15:16:53 +0100 Subject: [PATCH] Add simple fonctor for dot backend --- src/backend/dot.ml | 6 +++++- src/backend/dot.mli | 4 ++++ 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/src/backend/dot.ml b/src/backend/dot.ml index fdfec48f..0ef710c1 100644 --- a/src/backend/dot.ml +++ b/src/backend/dot.ml @@ -101,5 +101,9 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom and type lemma := S.lemm 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) diff --git a/src/backend/dot.mli b/src/backend/dot.mli index d47271a2..5e47032b 100644 --- a/src/backend/dot.mli +++ b/src/backend/dot.mli @@ -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 (** 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. *) +