Module ProverCoq

module ProverCoq: sig .. end

val dkey : Log.category
val cluster_file : Definitions.cluster -> string
val option_file : LogicBuiltins.doption
type coqlib = {
   c_id : string;
   c_source : string;
   c_file : string;
   c_path : string;
   c_name : string;
   c_module : string;
}
val name_of_path : string -> string
val find_nonwin_column : string -> int
val parse_c_option : string -> coqlib
val coqlibs : (string, coqlib) Hashtbl.t
val c_option : string -> coqlib
type depend = 
| D_cluster of Definitions.cluster
| D_coqlib of coqlib
val engine : < basename : string -> string; bind : Lang.F.var -> unit;
callstyle : Qed.Engine.callstyle; datatype : Lang.ADT.t -> string;
datatypename : string -> string; declare : string -> unit;
declare_all : string list -> unit;
declare_axiom : Format.formatter ->
string ->
Lang.F.var list ->
Definitions.trigger list list -> Lang.F.term -> unit;
declare_definition : Format.formatter ->
Lang.F.Fun.t ->
Lang.F.var list -> Lang.F.tau -> Lang.F.term -> unit;
declare_fixpoint : prefix:string ->
Format.formatter ->
Lang.F.Fun.t ->
Lang.F.var list -> Lang.F.tau -> Lang.F.term -> unit;
declare_signature : Format.formatter ->
Lang.F.Fun.t -> Lang.F.tau list -> Lang.F.tau -> unit;
declare_type : Format.formatter ->
Lang.F.ADT.t -> int -> Definitions.typedef -> unit;
e_false : Qed.Engine.cmode -> string; e_true : Qed.Engine.cmode -> string;
field : Lang.Field.t -> string; fieldname : string -> string;
funname : string -> string; global : (unit -> unit) -> unit;
infoprover : 'a. 'a Lang.infoprover -> 'a; is_atomic : Lang.F.term -> bool;
is_shareable : Lang.F.term -> bool; link : Lang.Fun.t -> Qed.Engine.link;
local : (unit -> unit) -> unit; mode : Qed.Engine.mode;
op_add : Qed.Engine.amode -> Qed.Engine.op;
op_and : Qed.Engine.cmode -> Qed.Engine.op;
op_div : Qed.Engine.amode -> Qed.Engine.op;
op_eq : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op;
op_equal : Qed.Engine.cmode -> Qed.Engine.op;
op_equiv : Qed.Engine.cmode -> Qed.Engine.op;
op_imply : Qed.Engine.cmode -> Qed.Engine.op;
op_leq : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op;
op_lt : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op;
op_minus : Qed.Engine.amode -> Qed.Engine.op;
op_mod : Qed.Engine.amode -> Qed.Engine.op;
op_mul : Qed.Engine.amode -> Qed.Engine.op;
op_neq : Qed.Engine.cmode -> Qed.Engine.amode -> Qed.Engine.op;
op_not : Qed.Engine.cmode -> Qed.Engine.op;
op_noteq : Qed.Engine.cmode -> Qed.Engine.op;
op_or : Qed.Engine.cmode -> Qed.Engine.op; op_real_of_int : Qed.Engine.op;
op_scope : Qed.Engine.amode -> string option; op_spaced : string -> bool;
op_sub : Qed.Engine.amode -> Qed.Engine.op;
pp_apply : Qed.Engine.cmode ->
Lang.F.term -> Lang.F.term list Qed.Plib.printer;
pp_array : Lang.F.tau Qed.Plib.printer;
pp_array_get : Format.formatter -> Lang.F.term -> Lang.F.term -> unit;
pp_array_set : Format.formatter ->
Lang.F.term -> Lang.F.term -> Lang.F.term -> unit;
pp_atom : Lang.F.term Qed.Plib.printer;
pp_conditional : Format.formatter ->
Lang.F.term -> Lang.F.term -> Lang.F.term -> unit;
pp_cst : Qed.Numbers.cst Qed.Plib.printer;
pp_datatype : Lang.F.ADT.t -> Lang.F.tau list Qed.Plib.printer;
pp_def_fields : (Lang.F.Field.t * Lang.F.term) list Qed.Plib.printer;
pp_equal : Lang.F.term Qed.Plib.printer2;
pp_exists : Lang.F.tau -> Lang.F.var list Qed.Plib.printer;
pp_expr : Lang.F.tau -> Lang.F.term Qed.Plib.printer;
pp_farray : Lang.F.tau Qed.Plib.printer2;
pp_flow : Lang.F.term Qed.Plib.printer;
pp_forall : Lang.F.tau -> Lang.F.var list Qed.Plib.printer;
pp_fun : Qed.Engine.cmode ->
Lang.F.Fun.t -> Lang.F.term list Qed.Plib.printer;
pp_get_field : Format.formatter -> Lang.F.term -> Lang.F.Field.t -> unit;
pp_imply : Format.formatter -> Lang.F.term list -> Lang.F.term -> unit;
pp_int : Qed.Engine.amode -> Lang.F.Z.t Qed.Plib.printer;
pp_lambda : Lang.F.var list Qed.Plib.printer;
pp_let : Format.formatter ->
Qed.Engine.pmode -> string -> Lang.F.term -> unit;
pp_not : Lang.F.term Qed.Plib.printer;
pp_noteq : Lang.F.term Qed.Plib.printer2;
pp_prop : Lang.F.term Qed.Plib.printer; pp_real : Qed.R.t Qed.Plib.printer;
pp_subtau : Lang.F.tau Qed.Plib.printer;
pp_tau : Lang.F.tau Qed.Plib.printer;
pp_term : Lang.F.term Qed.Plib.printer;
pp_times : Format.formatter -> Lang.F.Z.t -> Lang.F.term -> unit;
pp_tvar : int Qed.Plib.printer; pp_var : Lang.F.var Qed.Plib.printer;
t_atomic : Lang.F.tau -> bool; t_bool : string; t_int : string;
t_prop : string; t_real : string;
with_mode : Qed.Engine.mode -> (Qed.Engine.mode -> unit) -> unit >
class visitor : Format.formatter -> Definitions.cluster -> object .. end
val write_cluster : Definitions.cluster -> depend list
val need_recompile : source:string -> target:string -> bool
module CLUSTERS: Model.Index(sig
type key = Definitions.cluster 
type data = int * ProverCoq.depend list 
val name : string
val compare : Definitions.cluster -> Definitions.cluster -> int
val pretty : Format.formatter -> Definitions.cluster -> unit
end)
module Marked: Set.Make(sig
type t = ProverCoq.depend 
val compare : ProverCoq.depend -> ProverCoq.depend -> int
end)
type included = string * string 
type coqcc = {
   mutable marked : Marked.t;
   mutable includes : included list;
   mutable sources : string list;
}
val add_include : coqcc -> included -> unit
val add_source : coqcc -> string -> unit
val assemble : coqcc -> Marked.elt -> unit
val assemble_cluster : coqcc -> CLUSTERS.key -> unit
val assemble_coqlib : coqcc -> coqlib -> unit
val assemble_goal : pid:WpPropId.prop_id ->
Definitions.axioms option ->
Lang.F.pred -> included list * string list * string
val coq_timeout : unit -> Wp_parameters.CoqTimeout.t
val coqidelock : Task.mutex
class runcoq : (Wp_parameters.Script.t * Wp_parameters.Script.t) list -> Wp_parameters.Script.t -> object .. end
val shared_demon : bool Pervasives.ref
val shared_headers : (Wp_parameters.Script.t, unit Task.shared) Hashtbl.t
val shared : (Wp_parameters.Script.t * Wp_parameters.Script.t) list ->
Wp_parameters.Script.t -> unit Task.shared
val compile_headers : (Wp_parameters.Script.t * Wp_parameters.Script.t) list ->
bool -> Wp_parameters.Script.t list -> unit Task.task
type coq_wpo = {
   cw_pid : WpPropId.prop_id;
   cw_gid : string;
   cw_goal : string;
   cw_script : string;
   cw_headers : string list;
   cw_includes : included list;
}
val make_script : ?admitted:bool -> coq_wpo -> string -> unit
val try_script : ?admitted:bool -> coq_wpo -> string -> bool Task.task
val try_hints : coq_wpo -> (string * string) list -> bool Task.task
val try_prove : coq_wpo -> bool Task.task
val try_coqide : coq_wpo -> bool Task.task
val prove_session : mode:VCS.mode -> coq_wpo -> VCS.result Task.task
exception Admitted_not_proved
val check_session : coq_wpo -> VCS.result Task.task
val prove_session : mode:VCS.mode -> coq_wpo -> VCS.result Task.task
val prove_prop : Wpo.t ->
mode:VCS.mode ->
axioms:Definitions.axioms option -> prop:Lang.F.pred -> VCS.result Task.task
val prove_annot : Wpo.t -> Wpo.VC_Annot.t -> mode:VCS.mode -> VCS.result Task.task
val prove_lemma : Wpo.t -> Wpo.VC_Lemma.t -> mode:VCS.mode -> VCS.result Task.task
val prove_check : Wpo.t -> Wpo.VC_Check.t -> mode:VCS.mode -> VCS.result Task.task
val prove : VCS.mode -> Wpo.t -> VCS.result Task.task