Module Firstorder_plugin.Rules
type tactic= unit Proofview.tactictype seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactictype lseqtac= Names.GlobRef.t -> seqtactype 'a with_backtracking= tactic -> 'a
val wrap : int -> bool -> seqtacval clear_global : Names.GlobRef.t -> tacticval axiom_tac : EConstr.constr -> Sequent.t -> tacticval ll_atom_tac : EConstr.constr -> lseqtac with_backtrackingval and_tac : seqtac with_backtrackingval or_tac : seqtac with_backtrackingval arrow_tac : seqtac with_backtrackingval left_and_tac : Constr.pinductive -> lseqtac with_backtrackingval left_or_tac : Constr.pinductive -> lseqtac with_backtrackingval left_false_tac : Names.GlobRef.t -> tacticval ll_ind_tac : Constr.pinductive -> EConstr.constr list -> lseqtac with_backtrackingval ll_arrow_tac : EConstr.constr -> EConstr.constr -> EConstr.constr -> lseqtac with_backtrackingval forall_tac : seqtac with_backtrackingval left_exists_tac : Constr.pinductive -> lseqtac with_backtrackingval ll_forall_tac : EConstr.types -> lseqtac with_backtracking