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