package coq-core

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t
val priority : t -> int
val pattern : t -> Pattern.constr_pattern option
val database : t -> string option
val run : t -> (hint hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic
val name : t -> Names.GlobRef.t option
val print : Environ.env -> Evd.evar_map -> t -> Pp.t
val subgoals : t -> int option
val repr : t -> hint hint_ast

This function is for backward compatibility only, not to use in newly written code.

OCaml

Innovation. Community. Security.