summaryrefslogtreecommitdiff
path: root/tactics/hiddentac.mli
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2008-08-08 13:18:42 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2008-08-08 13:18:42 +0200
commit870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch)
tree0c647056de1832cf1dba5ba58758b9121418e4be /tactics/hiddentac.mli
parenta0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff)
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'tactics/hiddentac.mli')
-rw-r--r--tactics/hiddentac.mli33
1 files changed, 20 insertions, 13 deletions
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index eed3b1da..3e636668 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -6,10 +6,11 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: hiddentac.mli 11072 2008-06-08 16:13:37Z herbelin $ i*)
+(*i $Id: hiddentac.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
(*i*)
open Names
+open Util
open Term
open Proof_type
open Tacmach
@@ -25,7 +26,7 @@ open Clenv
(* Basic tactics *)
-val h_intro_move : identifier option -> identifier option -> tactic
+val h_intro_move : identifier option -> identifier move_location -> tactic
val h_intro : identifier -> tactic
val h_intros_until : quantified_hypothesis -> tactic
@@ -35,7 +36,7 @@ val h_exact_no_check : constr -> tactic
val h_vm_cast_no_check : constr -> tactic
val h_apply : advanced_flag -> evars_flag ->
- constr with_ebindings -> tactic
+ constr with_ebindings list -> tactic
val h_elim : evars_flag -> constr with_ebindings ->
constr with_ebindings option -> tactic
@@ -63,14 +64,20 @@ val h_instantiate : int -> Rawterm.rawconstr ->
val h_simple_induction : quantified_hypothesis -> tactic
val h_simple_destruct : quantified_hypothesis -> tactic
-val h_new_induction :
- evars_flag -> constr with_ebindings induction_arg list ->
- constr with_ebindings option -> intro_pattern_expr ->
- Tacticals.clause option -> tactic
-val h_new_destruct :
- evars_flag -> constr with_ebindings induction_arg list ->
- constr with_ebindings option -> intro_pattern_expr ->
- Tacticals.clause option -> tactic
+val h_simple_induction_destruct : rec_flag -> quantified_hypothesis -> tactic
+val h_new_induction : evars_flag ->
+ constr with_ebindings induction_arg list -> constr with_ebindings option ->
+ intro_pattern_expr located option * intro_pattern_expr located option ->
+ Tacticals.clause option -> tactic
+val h_new_destruct : evars_flag ->
+ constr with_ebindings induction_arg list -> constr with_ebindings option ->
+ intro_pattern_expr located option * intro_pattern_expr located option ->
+ Tacticals.clause option -> tactic
+val h_induction_destruct : rec_flag -> evars_flag ->
+ (constr with_ebindings induction_arg list * constr with_ebindings option *
+ (intro_pattern_expr located option * intro_pattern_expr located option) *
+ Tacticals.clause option) list -> tactic
+
val h_specialize : int option -> constr with_ebindings -> tactic
val h_lapply : constr -> tactic
@@ -80,7 +87,7 @@ val h_lapply : constr -> tactic
(* Context management *)
val h_clear : bool -> identifier list -> tactic
val h_clear_body : identifier list -> tactic
-val h_move : bool -> identifier -> identifier -> tactic
+val h_move : bool -> identifier -> identifier move_location -> tactic
val h_rename : (identifier*identifier) list -> tactic
val h_revert : identifier list -> tactic
@@ -110,4 +117,4 @@ val h_simplest_eapply : constr -> tactic
val h_simplest_elim : constr -> tactic
val h_simplest_case : constr -> tactic
-val h_intro_patterns : intro_pattern_expr list -> tactic
+val h_intro_patterns : intro_pattern_expr located list -> tactic