diff options
Diffstat (limited to 'plugins/decl_mode/decl_proof_instr.mli')
-rw-r--r-- | plugins/decl_mode/decl_proof_instr.mli | 109 |
1 files changed, 109 insertions, 0 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.mli b/plugins/decl_mode/decl_proof_instr.mli new file mode 100644 index 00000000..775d2f53 --- /dev/null +++ b/plugins/decl_mode/decl_proof_instr.mli @@ -0,0 +1,109 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Refiner +open Names +open Term +open Tacmach +open Decl_mode + +val go_to_proof_mode: unit -> unit +val return_from_tactic_mode: unit -> unit + +val register_automation_tac: tactic -> unit + +val automation_tac : tactic + +val concl_refiner: + Termops.meta_type_map -> constr -> Proof_type.goal sigma -> constr + +val do_instr: Decl_expr.raw_proof_instr -> Proof.proof -> unit +val proof_instr: Decl_expr.raw_proof_instr -> unit + +val tcl_change_info : Decl_mode.pm_info -> tactic + +val execute_cases : + Names.name -> + Decl_mode.per_info -> + (Term.constr -> Proof_type.tactic) -> + (Names.Idset.elt * (Term.constr option * Term.constr list) list) list -> + Term.constr list -> int -> Decl_mode.split_tree -> Proof_type.tactic + +val tree_of_pats : + identifier * (int * int) -> (Glob_term.cases_pattern*recpath) list list -> + split_tree + +val add_branch : + identifier * (int * int) -> (Glob_term.cases_pattern*recpath) list list -> + split_tree -> split_tree + +val append_branch : + identifier *(int * int) -> int -> (Glob_term.cases_pattern*recpath) list list -> + (Names.Idset.t * Decl_mode.split_tree) option -> + (Names.Idset.t * Decl_mode.split_tree) option + +val append_tree : + identifier * (int * int) -> int -> (Glob_term.cases_pattern*recpath) list list -> + split_tree -> split_tree + +val build_dep_clause : Term.types Decl_expr.statement list -> + Decl_expr.proof_pattern -> + Decl_mode.per_info -> + (Term.types Decl_expr.statement, Term.types Decl_expr.or_thesis) + Decl_expr.hyp list -> Proof_type.goal Tacmach.sigma -> Term.types + +val register_dep_subcase : + Names.identifier * (int * int) -> + Environ.env -> + Decl_mode.per_info -> + Glob_term.cases_pattern -> Decl_mode.elim_kind -> Decl_mode.elim_kind + +val thesis_for : Term.constr -> + Term.constr -> Decl_mode.per_info -> Environ.env -> Term.constr + +val close_previous_case : Proof.proof -> unit + +val pop_stacks : + (Names.identifier * + (Term.constr option * Term.constr list) list) list -> + (Names.identifier * + (Term.constr option * Term.constr list) list) list + +val push_head : Term.constr -> + Names.Idset.t -> + (Names.identifier * + (Term.constr option * Term.constr list) list) list -> + (Names.identifier * + (Term.constr option * Term.constr list) list) list + +val push_arg : Term.constr -> + (Names.identifier * + (Term.constr option * Term.constr list) list) list -> + (Names.identifier * + (Term.constr option * Term.constr list) list) list + +val hrec_for: + Names.identifier -> + Decl_mode.per_info -> Proof_type.goal Tacmach.sigma -> + Names.identifier -> Term.constr + +val consider_match : + bool -> + (Names.Idset.elt*bool) list -> + Names.Idset.elt list -> + (Term.types Decl_expr.statement, Term.types) Decl_expr.hyp list -> + Proof_type.tactic + +val init_tree: + Names.Idset.t -> + Names.inductive -> + int option * Declarations.wf_paths -> + (int -> + (int option * Declarations.recarg Rtree.t) array -> + (Names.Idset.t * Decl_mode.split_tree) option) -> + Decl_mode.split_tree |