Detyping (coq-core.Detyping)

type _ delay =

| Now : 'a delay

| Later : [ `thunk ] delay

val print_universes : bool Stdlib.ref

Should we keep details of universes during detyping ?

val print_evar_arguments : bool Stdlib.ref

If true, prints full local context of evars

val print_factorize_match_patterns : unit -> bool

If true, contract branches with same r.h.s. and same matching variables in a disjunctive pattern

val print_allow_match_default_clause : unit -> bool

If this flag is true and the last non unique clause of a "match" is a variable-free disjunctive pattern, turn it into a catch-call case

val print_allow_match_default_opt_name : string list

val subst_cases_pattern : 
  Mod_subst.substitution ->
  Glob_term.cases_pattern ->
  Glob_term.cases_pattern

val subst_glob_constr : 
  Environ.env ->
  Mod_subst.substitution ->
  Glob_term.glob_constr ->
  Glob_term.glob_constr

val factorize_eqns : 
  'a Glob_term.cases_clauses_g ->
  'a Glob_term.disjunctive_cases_clauses_g

detype isgoal avoid ctx c turns a closed c, into a glob_constr de Bruijn indexes are turned to bound names, avoiding names in avoid isgoal tells if naming must avoid global-level synonyms as intro does ctx gives the names of the free variables

val detype : 
  'a delay ->
  ?isgoal:bool ->
  Names.Id.Set.t ->
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  'a Glob_term.glob_constr_g

val detype_sort : Evd.evar_map -> Sorts.t -> Glob_term.glob_sort

val detype_rel_context : 
  'a delay ->
  EConstr.constr option ->
  Names.Id.Set.t ->
  (Termops.names_context * Environ.env) ->
  Evd.evar_map ->
  EConstr.rel_context ->
  'a Glob_term.glob_decl_g list

val share_pattern_names : 
  ( Names.Id.Set.t ->
    Termops.names_context ->
    'c ->
    Pattern.constr_pattern ->
    'a ) ->
  int ->
  (Names.Name.t * Glob_term.binding_kind * 'b option * 'a) list ->
  Names.Id.Set.t ->
  Termops.names_context ->
  'c ->
  Pattern.constr_pattern ->
  Pattern.constr_pattern ->
  (Names.Name.t * Glob_term.binding_kind * 'b option * 'a) list * 'a * 'a

val detype_closed_glob : 
  ?isgoal:bool ->
  Names.Id.Set.t ->
  Environ.env ->
  Evd.evar_map ->
  Ltac_pretype.closed_glob_constr ->
  Glob_term.glob_constr

val lookup_name_as_displayed : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  Names.Id.t ->
  int option

look for the index of a named var or a nondep var as it is renamed

val lookup_index_as_renamed : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  int ->
  int option

val force_wildcard : unit -> bool

val synthetize_type : unit -> bool

val subst_genarg_hook : 
  ( Mod_subst.substitution ->
    Genarg.glob_generic_argument ->
    Genarg.glob_generic_argument )
    Hook.t

module PrintingInductiveMake (Test : sig ... end) : sig ... end