package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val print_universes : bool Pervasives.ref
val print_evar_arguments : bool Pervasives.ref
val detype : ?lax:bool -> bool -> Names.Id.t list -> Environ.env -> Evd.evar_map -> EConstr.constr -> Glob_term.glob_constr
val detype_rel_context : ?lax:bool -> EConstr.constr option -> Names.Id.t list -> (Termops.names_context * Environ.env) -> Evd.evar_map -> EConstr.rel_context -> Glob_term.glob_decl list
val detype_closed_glob : ?lax:bool -> bool -> Names.Id.t list -> Environ.env -> Evd.evar_map -> Glob_term.closed_glob_constr -> Glob_term.glob_constr
val lookup_name_as_displayed : Environ.env -> Evd.evar_map -> EConstr.constr -> Names.Id.t -> int option
val lookup_index_as_renamed : Environ.env -> Evd.evar_map -> EConstr.constr -> int -> int option
val set_detype_anonymous : (?loc:Loc.t -> int -> Glob_term.glob_constr) -> unit
val force_wildcard : unit -> bool
val synthetize_type : unit -> bool
val it_destRLambda_or_LetIn_names : bool list -> Glob_term.glob_constr -> Names.Name.t list * Glob_term.glob_constr
val simple_cases_matrix_of_branches : Names.inductive -> (int * bool list * Glob_term.glob_constr) list -> Glob_term.cases_clauses
val return_type_of_predicate : Names.inductive -> bool list -> Glob_term.glob_constr -> Glob_term.predicate_pattern * Glob_term.glob_constr option
module PrintingInductiveMake (Test : sig ... end) : sig ... end
OCaml

Innovation. Community. Security.