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