diff options
Diffstat (limited to 'contrib/subtac/subtac_obligations.mli')
| -rw-r--r-- | contrib/subtac/subtac_obligations.mli | 34 |
1 files changed, 28 insertions, 6 deletions
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli index f015b80b..6d13e3bd 100644 --- a/contrib/subtac/subtac_obligations.mli +++ b/contrib/subtac/subtac_obligations.mli @@ -1,22 +1,42 @@ +open Names open Util +open Libnames -type obligation_info = (Names.identifier * Term.types * bool * Intset.t) array - (* ident, type, opaque or transparent, dependencies *) +type obligation_info = (Names.identifier * Term.types * loc * bool * Intset.t) array + (* ident, type, location, opaque or transparent, dependencies *) +type progress = (* Resolution status of a program *) + | Remain of int (* n obligations remaining *) + | Dependent (* Dependent on other definitions *) + | Defined of global_reference (* Defined as id *) + val set_default_tactic : Tacexpr.glob_tactic_expr -> unit val default_tactic : unit -> Proof_type.tactic +val set_proofs_transparency : bool -> unit (* true = All transparent, false = Opaque if possible *) +val get_proofs_transparency : unit -> bool + +type definition_hook = global_reference -> unit + val add_definition : Names.identifier -> Term.constr -> Term.types -> - obligation_info -> unit + ?implicits:(Topconstr.explicitation * (bool * bool)) list -> + ?kind:Decl_kinds.definition_kind -> + ?hook:definition_hook -> obligation_info -> progress + +type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list val add_mutual_definitions : - (Names.identifier * Term.constr * Term.types * obligation_info) list -> int array -> unit + (Names.identifier * Term.constr * Term.types * + (Topconstr.explicitation * (bool * bool)) list * obligation_info) list -> + ?kind:Decl_kinds.definition_kind -> + notations -> + Command.fixpoint_kind -> unit val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr option -> unit val next_obligation : Names.identifier option -> unit -val solve_obligations : Names.identifier option -> Proof_type.tactic -> int +val solve_obligations : Names.identifier option -> Proof_type.tactic -> progress (* Number of remaining obligations to be solved for this program *) val solve_all_obligations : Proof_type.tactic -> unit @@ -25,7 +45,9 @@ val try_solve_obligation : int -> Names.identifier option -> Proof_type.tactic - val try_solve_obligations : Names.identifier option -> Proof_type.tactic -> unit -val show_obligations : Names.identifier option -> unit +val show_obligations : ?msg:bool -> Names.identifier option -> unit + +val show_term : Names.identifier option -> unit val admit_obligations : Names.identifier option -> unit |