(* Coq printing functions for model-checking h1 clauses in Seidl form, headers.
   Copyright (C) 2003 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 "seidl_h";
open "model_h";

extern val coq_seidl_mc : ('a outstream * string * string
			   * (''var -> string) * (''var set -m> ''var list)
			   * string * string
			   * (''var gclause -> string option))
	   -> ''var approx_justif_and_clause -> string option;

(* coq_seidl_mc (fd, fun_prefix, state_prefix, varname, varsort,
                 term_type, rem_name, mc) j_c
 tries to output Coq justification of general clause j_c
 in model whose model-checker is mc [mc should also print Coq proofs]
 on file fd; predicates are prefixed with state_prefix;
 functions are prefixed with fun_prefix;
 varname is a function returning names of variables;
 varsort sorts variables in ascending order;
 term_type is the type of terms;
 rem_name is the common prefix of all intermediate Remarks.
 *)
