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..1205060a
--- /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-2010     *)
+(*   \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