tactics/dhyp.mli


1
2
3
4
5
6
7
8
9
10
11
12


(* $Id$ *)

(*i*)
open Names
open Tacmach
(*i*)

(* Programmable destruction of hypotheses and conclusions. *)

val dHyp : identifier -> tactic
val dConcl : tactic