1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: rules.mli 6141 2004-09-27 14:55:34Z corbinea $ *)
16
type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
18
type lseqtac= global_reference -> seqtac
20
type 'a with_backtracking = tactic -> 'a
22
val wrap : int -> bool -> seqtac
24
val id_of_global: global_reference -> identifier
26
val clear_global: global_reference -> tactic
28
val axiom_tac : constr -> Sequent.t -> tactic
30
val ll_atom_tac : constr -> lseqtac with_backtracking
32
val and_tac : seqtac with_backtracking
34
val or_tac : seqtac with_backtracking
36
val arrow_tac : seqtac with_backtracking
38
val left_and_tac : inductive -> lseqtac with_backtracking
40
val left_or_tac : inductive -> lseqtac with_backtracking
42
val left_false_tac : global_reference -> tactic
44
val ll_ind_tac : inductive -> constr list -> lseqtac with_backtracking
46
val ll_arrow_tac : constr -> constr -> constr -> lseqtac with_backtracking
48
val forall_tac : seqtac with_backtracking
50
val left_exists_tac : inductive -> lseqtac with_backtracking
52
val ll_forall_tac : types -> lseqtac with_backtracking
54
val normalize_evaluables : tactic