diff options
Diffstat (limited to 'src/tac2tactics.mli')
| -rw-r--r-- | src/tac2tactics.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli index 5fdd1c39bc..8e15fb1392 100644 --- a/src/tac2tactics.mli +++ b/src/tac2tactics.mli @@ -63,6 +63,10 @@ type rewriting = multi * constr_with_bindings tactic +type assertion = +| AssertType of intro_pattern option * constr * unit tactic option +| AssertValue of Id.t * constr + (** Local reimplementations of tactics variants from Coq *) val intros_patterns : evars_flag -> intro_pattern list -> unit tactic @@ -91,6 +95,8 @@ val rewrite : val forward : bool -> unit tactic option option -> intro_pattern option -> constr -> unit tactic +val assert_ : assertion -> unit tactic + val letin_pat_tac : evars_flag -> (bool * intro_pattern_naming) option -> Name.t -> (Evd.evar_map * constr) -> clause -> unit tactic |