From 8eee822ad69249c6721927e092108220c6964725 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Tue, 22 Aug 2017 14:55:21 +0200
Subject: [PATCH] Removed some unused code in coq backend

---
 src/backend/coq.ml  | 30 ++----------------------------
 src/backend/coq.mli | 12 ++----------
 2 files changed, 4 insertions(+), 38 deletions(-)

diff --git a/src/backend/coq.ml b/src/backend/coq.ml
index 43f618b8..235f2b27 100644
--- a/src/backend/coq.ml
+++ b/src/backend/coq.ml
@@ -7,22 +7,17 @@ module type S = Backend_intf.S
 
 module type Arg = sig
 
-  type atom
-
   type hyp
   type lemma
   type assumption
 
-  val print_atom : Format.formatter -> atom -> unit
-
   val prove_hyp : Format.formatter -> string -> hyp -> unit
   val prove_lemma : Format.formatter -> string -> lemma -> unit
   val prove_assumption : Format.formatter -> string -> assumption -> unit
 
 end
 
-module Make(S : Res.S)(A : Arg with type atom := S.atom
-                                and type hyp := S.clause
+module Make(S : Res.S)(A : Arg with type hyp := S.clause
                                 and type lemma := S.clause
                                 and type assumption := S.clause) = struct
 
@@ -33,22 +28,6 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
 
   let name c = c.S.St.name
 
-  let pp_atom fmt a =
-    if a == S.St.(a.var.pa) then
-      Format.fprintf fmt "~ %a" A.print_atom a
-    else
-      Format.fprintf fmt "~ ~ %a" A.print_atom a.S.St.neg
-
-  let pp_clause fmt c =
-    let rec aux fmt (a, i) =
-      if i < Array.length a then
-        Format.fprintf fmt "%a ->@ %a"
-          pp_atom a.(i) aux (a, i + 1)
-      else
-        Format.fprintf fmt "False"
-    in
-    Format.fprintf fmt "@[<hov 1>(%a)@]" aux (c.S.St.atoms, 0)
-
   let clause_map c =
     let rec aux acc a i =
       if i >= Array.length a then acc
@@ -141,8 +120,7 @@ end
 
 
 module Simple(S : Res.S)
-    (A : Arg with type atom := S.St.formula
-              and type hyp = S.St.formula list
+    (A : Arg with type hyp = S.St.formula list
               and type lemma := S.lemma
               and type assumption := S.St.formula) =
   Make(S)(struct
@@ -160,10 +138,6 @@ module Simple(S : Res.S)
       | S.St.Lemma p -> p
       | _ -> assert false
 
-    (* Actual functions *)
-    let print_atom fmt a =
-      A.print_atom fmt a.S.St.lit
-
     let prove_hyp fmt name c =
       A.prove_hyp fmt name (List.map lit (S.to_list c))
 
diff --git a/src/backend/coq.mli b/src/backend/coq.mli
index 9d26b806..61c42785 100644
--- a/src/backend/coq.mli
+++ b/src/backend/coq.mli
@@ -15,17 +15,11 @@ module type S = Backend_intf.S
 module type Arg = sig
   (** Term printing for Coq *)
 
-  type atom
-  (** The type of atomic formulas *)
-
   type hyp
   type lemma
   type assumption
   (** The types of hypotheses, lemmas, and assumptions *)
 
-  val print_atom : Format.formatter -> atom -> unit
-  (** Print the given atomic formula *)
-
   val prove_hyp : Format.formatter -> string -> hyp -> unit
   val prove_lemma : Format.formatter -> string -> lemma -> unit
   val prove_assumption : Format.formatter -> string -> assumption -> unit
@@ -39,15 +33,13 @@ module type Arg = sig
 
 end
 
-module Make(S : Res.S)(A : Arg with type atom := S.atom
-                                and type hyp := S.clause
+module Make(S : Res.S)(A : Arg with type hyp := S.clause
                                 and type lemma := S.clause
                                 and type assumption := S.clause) : S with type t := S.proof
 (** Base functor to output Coq proofs *)
 
 
-module Simple(S : Res.S)(A : Arg with type atom := S.St.formula
-                                  and type hyp = S.St.formula list
+module Simple(S : Res.S)(A : Arg with type hyp = S.St.formula list
                                   and type lemma := S.lemma
                                   and type assumption := S.St.formula) : S with type t := S.proof
 (** Simple functo to output Coq proofs *)