summaryrefslogtreecommitdiff
path: root/proofs/tacmach.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/tacmach.mli')
-rw-r--r--proofs/tacmach.mli17
1 files changed, 8 insertions, 9 deletions
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 8b0053a4..2fc66e71 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: tacmach.mli 11094 2008-06-10 19:35:23Z herbelin $ i*)
+(*i $Id: tacmach.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
(*i*)
open Names
@@ -123,15 +123,15 @@ val change_constraints_pftreestate :
val refiner : rule -> tactic
val introduction_no_check : identifier -> tactic
-val intro_replacing_no_check : identifier -> tactic
-val internal_cut_no_check : identifier -> types -> tactic
-val internal_cut_rev_no_check : identifier -> types -> tactic
+val internal_cut_no_check : bool -> identifier -> types -> tactic
+val internal_cut_rev_no_check : bool -> identifier -> types -> tactic
val refine_no_check : constr -> tactic
val convert_concl_no_check : types -> cast_kind -> tactic
val convert_hyp_no_check : named_declaration -> tactic
val thin_no_check : identifier list -> tactic
val thin_body_no_check : identifier list -> tactic
-val move_hyp_no_check : bool -> identifier -> identifier -> tactic
+val move_hyp_no_check :
+ bool -> identifier -> identifier move_location -> tactic
val rename_hyp_no_check : (identifier*identifier) list -> tactic
val mutual_fix :
identifier -> int -> (identifier * int * constr) list -> tactic
@@ -140,15 +140,14 @@ val mutual_cofix : identifier -> (identifier * constr) list -> tactic
(*s The most primitive tactics with consistency and type checking *)
val introduction : identifier -> tactic
-val intro_replacing : identifier -> tactic
-val internal_cut : identifier -> types -> tactic
-val internal_cut_rev : identifier -> types -> tactic
+val internal_cut : bool -> identifier -> types -> tactic
+val internal_cut_rev : bool -> identifier -> types -> tactic
val refine : constr -> tactic
val convert_concl : types -> cast_kind -> tactic
val convert_hyp : named_declaration -> tactic
val thin : identifier list -> tactic
val thin_body : identifier list -> tactic
-val move_hyp : bool -> identifier -> identifier -> tactic
+val move_hyp : bool -> identifier -> identifier move_location -> tactic
val rename_hyp : (identifier*identifier) list -> tactic
(*s Tactics handling a list of goals. *)