Module `Detyping`Source

Sourcetype _ delay =

| Now : 'a delay
| Later : [ `thunk ] delay

Sourceval print_universes : bool ref

Should we keep details of universes during detyping ?

Sourceval print_evar_arguments : bool ref

If true, prints full local context of evars

Sourceval print_factorize_match_patterns : unit -> bool

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

Sourceval 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

Sourceval print_allow_match_default_opt_name : string list

Source

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

Source

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

Source

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

Source

val detype : 
  'a delay ->
  ?isgoal:bool ->
  ?avoid:'g Namegen.Generator.input ->
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  'a Glob_term.glob_constr_g

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

Source

val detype_rel_context : 
  'a delay ->
  EConstr.constr option ->
  ?avoid:'g Namegen.Generator.input ->
  (Termops.names_context * Environ.env) ->
  Evd.evar_map ->
  EConstr.rel_context ->
  'a Glob_term.glob_decl_g list

Source

val share_pattern_names : 
  ('g Namegen.Generator.input ->
    Termops.names_context ->
    'c ->
    'd Pattern.constr_pattern_r ->
    'a) ->
  int ->
  (Names.Name.t * 'e option * Glob_term.binding_kind * 'b option * 'a) list ->
  'g Namegen.Generator.input ->
  Termops.names_context ->
  'c ->
  'd Pattern.constr_pattern_r ->
  'd Pattern.constr_pattern_r ->
  (Names.Name.t * 'e option * Glob_term.binding_kind * 'b option * 'a) list
  * 'a
  * 'a

Source

val detype_closed_glob : 
  ?isgoal:bool ->
  ?avoid:'g Namegen.Generator.input ->
  Environ.env ->
  Evd.evar_map ->
  Ltac_pretype.closed_glob_constr ->
  Glob_term.glob_constr

Source

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

Source

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

Sourceval force_wildcard : unit -> bool

Sourceval synthetize_type : unit -> bool

Source

module PrintingInductiveMake
  (_ : sig ... end) : 
  Goptions.RefConvertArg
    with type t = Names.inductive
     and module Set = Names.Indset

Install

Dune Dependency

Authors

Maintainers

Sources

doc/rocq-runtime.pretyping/Detyping/index.html

Module `Detyping`Source

package rocq-runtime

Install

Dune Dependency

Authors

Maintainers

Sources

doc/rocq-runtime.pretyping/Detyping/index.html

Module DetypingSource

Module `Detyping`Source