diff options
Diffstat (limited to 'tactics/decl_proof_instr.mli')
| -rw-r--r-- | tactics/decl_proof_instr.mli | 87 |
1 files changed, 39 insertions, 48 deletions
diff --git a/tactics/decl_proof_instr.mli b/tactics/decl_proof_instr.mli index 642f2755..2e235a01 100644 --- a/tactics/decl_proof_instr.mli +++ b/tactics/decl_proof_instr.mli @@ -6,12 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: decl_proof_instr.mli 10739 2008-04-01 14:45:20Z herbelin $ *) 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 @@ -22,6 +23,8 @@ val automation_tac : tactic val daimon_subtree: pftreestate -> pftreestate +val concl_refiner: Termops.metamap -> constr -> Proof_type.goal sigma -> constr + val do_instr: Decl_expr.raw_proof_instr -> pftreestate -> pftreestate val proof_instr: Decl_expr.raw_proof_instr -> unit @@ -31,37 +34,29 @@ val mark_proof_tree_as_done : Proof_type.proof_tree -> Proof_type.proof_tree val mark_as_done : pftreestate -> pftreestate -val execute_cases : bool -> +val execute_cases : Names.name -> Decl_mode.per_info -> (Term.constr -> Proof_type.tactic) -> - (Names.Idset.elt * (Term.constr option * bool * Term.constr list) list) - list -> - Decl_mode.split_tree -> 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 -> (Rawterm.cases_pattern*recpath) list list -> + split_tree + +val add_branch : + identifier * int -> (Rawterm.cases_pattern*recpath) list list -> + split_tree -> split_tree -val tree_of_pats : - Environ.env -> - Names.Idset.elt * int -> - Rawterm.cases_pattern list list -> Decl_mode.split_tree -val add_branch : - Environ.env -> - Names.Idset.elt * int -> - Rawterm.cases_pattern list list -> - Decl_mode.split_tree -> Decl_mode.split_tree val append_branch : - Environ.env -> - Names.Idset.elt * int -> - int -> - Rawterm.cases_pattern list list -> - int -> - (Names.Idset.t * Decl_mode.split_tree) option -> - (Names.Idset.t * Decl_mode.split_tree) option - -val append_tree : Environ.env -> - Names.Idset.elt * int -> - int -> - Rawterm.cases_pattern list list -> - Decl_mode.split_tree -> Decl_mode.split_tree + identifier * int -> int -> (Rawterm.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 -> (Rawterm.cases_pattern*recpath) list list -> + split_tree -> split_tree val build_dep_clause : Term.types Decl_expr.statement list -> Decl_expr.proof_pattern -> @@ -80,35 +75,29 @@ val thesis_for : Term.constr -> val close_previous_case : pftreestate -> pftreestate -val test_fun : string -> unit - - val pop_stacks : (Names.identifier * - (Term.constr option * bool * Term.constr list) list) list -> - bool * - (Names.identifier * - (Term.constr option * bool * Term.constr list) list) list - + (Term.constr option * Term.constr list) list) list -> + (Names.identifier * + (Term.constr option * Term.constr list) list) list val push_head : Term.constr -> - bool -> Names.Idset.t -> (Names.identifier * - (Term.constr option * bool * Term.constr list) list) list -> + (Term.constr option * Term.constr list) list) list -> (Names.identifier * - (Term.constr option * bool * Term.constr list) list) list + (Term.constr option * Term.constr list) list) list val push_arg : Term.constr -> (Names.identifier * - (Term.constr option * bool * Term.constr list) list) list -> + (Term.constr option * Term.constr list) list) list -> (Names.identifier * - (Term.constr option * bool * Term.constr list) list) list + (Term.constr option * Term.constr list) list) list val hrec_for: Names.identifier -> - Names.identifier -> - Decl_mode.per_info -> Proof_type.goal Tacmach.sigma -> Term.constr option + Decl_mode.per_info -> Proof_type.goal Tacmach.sigma -> + Names.identifier -> Term.constr val consider_match : bool -> @@ -117,10 +106,12 @@ val consider_match : (Term.types Decl_expr.statement, Term.types) Decl_expr.hyp list -> Proof_type.tactic -val thus_tac : constr -> constr -> (metavariable * types) list -> - tactic - -val build_applist : Term.types -> - Term.metavariable list -> - (Term.metavariable * Term.types) list * Term.types +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 |