Module `Detyping`Source

Sourcetype _ delay =

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

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 : 
  flags:PrintingFlags.Extern.FactorizeEqns.t ->
  '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 ->
  flags:PrintingFlags.Detype.t ->
  ?isgoal:bool ->
  ?avoid:'g Namegen.Generator.input ->
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  'a Glob_term.glob_constr_g

Source

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

Source

val detype_rel_context : 
  'a delay ->
  flags:PrintingFlags.Detype.t ->
  ?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 : 
  flags:PrintingFlags.Detype.t ->
  ?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

Install

dune-project
Dependency

Authors

Maintainers

Sources

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

Module `Detyping`Source

package rocq-runtime

Install

dune-project Dependency

Authors

Maintainers

Sources

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

Module DetypingSource

dune-project
Dependency

Module `Detyping`Source