Module `Funind_plugin.G_indfun`Source

Source

val pr_fun_ind_using : 
  'a ->
  'b ->
  ('a -> 'b -> 'c -> Pp.t) ->
  ('a -> 'b -> 'c -> Pp.t) ->
  'd ->
  ('c * 'c Tactypes.bindings) option ->
  Pp.t

Source

val pr_fun_ind_using_typed : 
  (Environ.env -> Evd.evar_map -> 'a -> Pp.t) ->
  (Environ.env -> Evd.evar_map -> 'a -> Pp.t) ->
  'b ->
  (Environ.env -> Evd.evar_map -> 'c * ('a * 'a Tactypes.bindings)) option ->
  Pp.t

Source

val wit_fun_ind_using : 
  (Constrexpr.constr_expr Tactypes.with_bindings option,
    Genintern.glob_constr_and_expr Tactypes.with_bindings option,
    EConstr.constr Tactypes.with_bindings Tactypes.delayed_open option)
    Genarg.genarg_type

Source

val fun_ind_using : 
  Constrexpr.constr_expr Tactypes.with_bindings option Pcoq.Entry.t

Source

val pr_intro_as_pat : 
  ('a -> Pp.t) ->
  'a Tactypes.intro_pattern_expr CAst.t option ->
  Pp.t

Source

val out_disjunctive : 
  Tactypes.delayed_open_constr Tactypes.intro_pattern_expr CAst.t ->
  Tactypes.delayed_open_constr Tactypes.or_and_intro_pattern_expr CAst.t

Source

val wit_with_names : 
  (Constrexpr.constr_expr Tactypes.intro_pattern_expr CAst.t option,
    Genintern.glob_constr_and_expr Tactypes.intro_pattern_expr CAst.t option,
    Ltac_plugin.Tacexpr.intro_pattern option)
    Genarg.genarg_type

Source

val with_names : 
  Constrexpr.constr_expr Tactypes.intro_pattern_expr CAst.t option Pcoq.Entry.t

Source

val functional_induction : 
  'a ->
  EConstr.constr ->
  (EConstr.constr * EConstr.constr Tactypes.bindings) option ->
  Tactypes.delayed_open_constr Tactypes.intro_pattern_expr CAst.t option ->
  unit Proofview.tactic

Source

val pr_constr_comma_sequence : 
  'a ->
  'b ->
  ('a -> 'b -> 'c -> Pp.t) ->
  'd ->
  'e ->
  'c list ->
  Pp.t

Source

val wit_constr_comma_sequence' : 
  (Constrexpr.constr_expr list,
    Genintern.glob_constr_and_expr list,
    EConstr.constr list)
    Genarg.genarg_type

Sourceval constr_comma_sequence' : Constrexpr.constr_expr list Pcoq.Entry.t

Source

val pr_auto_using : 
  'a ->
  'b ->
  ('a -> 'b -> 'c -> Pp.t) ->
  'd ->
  'e ->
  'c list ->
  Pp.t

Source

val wit_auto_using' : 
  (Constrexpr.constr_expr list,
    Genintern.glob_constr_and_expr list,
    EConstr.constr list)
    Genarg.genarg_type

Sourceval auto_using' : Constrexpr.constr_expr list Pcoq.Entry.t

module Vernac = Pvernac.Vernac_

module Tactic = Ltac_plugin.Pltac

Source

val wit_function_fix_definition : 
  Vernacexpr.fixpoint_expr Loc.located Genarg.uniform_genarg_type

Sourceval function_fix_definition : Vernacexpr.fixpoint_expr Loc.located Pcoq.Entry.t

Source

val is_proof_termination_interactively_checked : 
  ('a * Constrexpr.recursion_order_expr_r CAst.t option Vernacexpr.fix_expr_gen)
    list ->
  bool

Source

val classify_as_Fixpoint : 
  ('a * Vernacexpr.fixpoint_expr) list ->
  Vernacextend.vernac_classification

Source

val classify_funind : 
  ('a * Vernacexpr.fixpoint_expr) list ->
  Vernacextend.vernac_classification

Sourceval is_interactive : ('a * Vernacexpr.fixpoint_expr) list -> bool

Sourceval pr_fun_scheme_arg : (Names.Id.t * Libnames.qualid * Sorts.family) -> Pp.t

Source

val wit_fun_scheme_arg : 
  (Names.Id.t * Libnames.qualid * Sorts.family, unit, unit) Genarg.genarg_type

Sourceval fun_scheme_arg : (Names.Id.t * Libnames.qualid * Sorts.family) Pcoq.Entry.t

Sourceval warning_error : Libnames.qualid list -> exn -> unit

Install

Dune Dependency

Authors

Maintainers

Sources

doc/funind_plugin/Funind_plugin/G_indfun/index.html

Module `Funind_plugin.G_indfun`Source

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/funind_plugin/Funind_plugin/G_indfun/index.html

Module Funind_plugin.G_indfunSource

Module `Funind_plugin.G_indfun`Source