Module Proof

module Proof: sig .. end
Coq Proof Scripts

val is_empty_script : string -> bool
Check a proof script text for emptyness
val delete_script_for : gid:string -> unit
delete_script ~gid remove known script for goal.
val add_script_for : gid:string -> string list -> string -> string -> unit
new_script goal keys proof qed registers the script proof terminated by qed for goal gid and keywords keys
val parse_coqproof : string -> (string * string) option
parse_coqproof f parses a coq-file f and fetch the first proof.
val savescripts : unit -> unit
If necessary, dump the scripts database into the file specified by -wp-script f.
val script_for : pid:WpPropId.prop_id ->
gid:string -> legacy:string -> (string * string) option
val script_for_ide : pid:WpPropId.prop_id -> gid:string -> legacy:string -> string * string
val hints_for : pid:WpPropId.prop_id -> (string * string * string) list