package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val __coq_plugin_name : string
type constr_expr_with_bindings = Constrexpr.constr_expr Tactypes.with_bindings
val pr_glob_constr_with_bindings_sign : Environ.env -> Evd.evar_map -> 'a -> 'b -> 'c -> glob_constr_with_bindings_sign -> Pp.t
val pr_glob_constr_with_bindings : Environ.env -> Evd.evar_map -> 'a -> 'b -> 'c -> glob_constr_with_bindings -> Pp.t
val pr_constr_expr_with_bindings : 'a -> 'b -> ('a -> 'b -> Constrexpr.constr_expr -> 'c) -> 'd -> 'e -> constr_expr_with_bindings -> 'c
val interp_glob_constr_with_bindings : 'a -> Goal.goal Evd.sigma -> 'b -> Evd.evar_map * ('a * 'b)
val subst_strategy : 'a -> 'b -> 'b
val pr_strategy : 'a -> 'b -> 'c -> Rewrite.strategy -> Pp.t
val rewstrategy : raw_strategy Pcoq.Entry.t
val db_strat : string -> ('a, 'b) Rewrite.strategy_ast
val cl_rewrite_clause_db : Tacinterp.interp_sign -> string -> Names.Id.t option -> unit Proofview.tactic
type binders_argtype = Constrexpr.local_binder_expr list
OCaml

Innovation. Community. Security.