(* print natural deduction proof in Coq format, headers.
   Copyright (C) 2003, 2008 Jean Goubault-Larrecq and LSV, CNRS UMR 8643 & ENS Cachan.

   This file is part of h1.

   h1 is free software; you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation; either version 2, or (at your option)
   any later version.

   h1 is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with h1; see the file COPYING.  If not, write to
   the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
*)

open "natded_h";

exception PfcCoqNoNameEvt;
exception PfcCoqAbortEvt;

extern val pfc_print_coq_proofs : string * 'a outstream * string * string
	   * string * string
	   * (string gclause -> string) * (string gclause -> string)
	   * (string * string gclause -> unit)
	   * (string -> string) * (string set -> string list)
	   * string
	   * (string * string gclause * pfabs) list -> unit;
(* pfc_print_coq_proofs (ver, f, thm_kwd, thm_prefix, fun_prefix, state_prefix,
                         defnames, assnames, do_abort,
                         varname, varsort, term_type, pfal)
 prints the proofs in pfal on file f.
 Each theorem is introduced by thm_kwd (e.g., "Theorem"), and
 its name is prefixed with thm_prefix.
 defnames and assnames provide external names to proofs of definitions
 and input clauses, respectively.  They may raise PfcCoqNoNameEvt
 to signal that no name exists for the corresponding clause, and that
 an Axiom should be created, or PfcCoqAbortEvt to signal that no name
 exists for the corresponding clause, and the proof of the given pfa
 in pfal should be aborted.  In the latter case, do_abort will be called
 on the source clause name that can be proved.
 pfal contains lists of tuples (clause-name, clause, proof).
*)

extern val pfc_print_coq : string * 'a outstream * string * string
	   * string * string
	   * string gclause set * string gclause set
	   * (string -> string) * (string set -> string list)
	   * string * pfc list -> unit;
(* pfc_print_coq (coq_version, f, thm_kwd, thm_prefix,fun_prefix, state_prefix,
                  definitions, input, varname, varsort, term_type, pfcl)
 prints the proofs in pfcl on file f.
 Definitions (in definitions) are posited using the keyword 'Definition'.
 Clauses (in input) are assumed using the keyword 'Axiom'.
 *)

