Module `Ltac2_plugin.Tac2quote`Source

Syntactic quoting of expressions.

Contrarily to Tac2ffi, which lives on the semantic level, this module manipulates pure syntax of Ltac2. Its main purpose is to write notations.

Source

val constructor : 
  ?loc:Loc.t ->
  Tac2expr.ltac_constructor ->
  Tac2expr.raw_tacexpr list ->
  Tac2expr.raw_tacexpr

Sourceval thunk : Tac2expr.raw_tacexpr -> Tac2expr.raw_tacexpr

Source

val of_anti : 
  ('a -> Tac2expr.raw_tacexpr) ->
  'a Tac2qexpr.or_anti ->
  Tac2expr.raw_tacexpr

Sourceval of_int : int CAst.t -> Tac2expr.raw_tacexpr

Source

val of_pair : 
  ('a -> Tac2expr.raw_tacexpr) ->
  ('b -> Tac2expr.raw_tacexpr) ->
  ('a * 'b) CAst.t ->
  Tac2expr.raw_tacexpr

Sourceval of_tuple : ?loc:Loc.t -> Tac2expr.raw_tacexpr list -> Tac2expr.raw_tacexpr

Sourceval of_variable : Names.Id.t CAst.t -> Tac2expr.raw_tacexpr

Sourceval of_ident : Names.Id.t CAst.t -> Tac2expr.raw_tacexpr

Source

val of_constr : 
  ?delimiters:Names.Id.t list ->
  Constrexpr.constr_expr ->
  Tac2expr.raw_tacexpr

Source

val of_open_constr : 
  ?delimiters:Names.Id.t list ->
  Constrexpr.constr_expr ->
  Tac2expr.raw_tacexpr

Source

val of_preterm : 
  ?delimiters:Names.Id.t list ->
  Constrexpr.constr_expr ->
  Tac2expr.raw_tacexpr

Source

val of_list : 
  ?loc:Loc.t ->
  ('a -> Tac2expr.raw_tacexpr) ->
  'a list ->
  Tac2expr.raw_tacexpr

Sourceval array_of_list : ?loc:Loc.t -> Tac2expr.raw_tacexpr -> Tac2expr.raw_tacexpr

Sourceval of_bindings : Tac2qexpr.bindings -> Tac2expr.raw_tacexpr

Sourceval of_intro_pattern : Tac2qexpr.intro_pattern -> Tac2expr.raw_tacexpr

Source

val of_intro_patterns : 
  Tac2qexpr.intro_pattern list CAst.t ->
  Tac2expr.raw_tacexpr

Sourceval of_clause : Tac2qexpr.clause -> Tac2expr.raw_tacexpr

Sourceval of_destruction_arg : Tac2qexpr.destruction_arg -> Tac2expr.raw_tacexpr

Sourceval of_induction_clause : Tac2qexpr.induction_clause -> Tac2expr.raw_tacexpr

Sourceval of_conversion : Tac2qexpr.conversion -> Tac2expr.raw_tacexpr

Sourceval of_orient : Tac2qexpr.orientation -> Tac2expr.raw_tacexpr

Sourceval of_rewriting : Tac2qexpr.rewriting -> Tac2expr.raw_tacexpr

Sourceval of_occurrences : Tac2qexpr.occurrences -> Tac2expr.raw_tacexpr

Sourceval of_hintdb : Tac2qexpr.hintdb -> Tac2expr.raw_tacexpr

Sourceval of_move_location : Tac2qexpr.move_location -> Tac2expr.raw_tacexpr

Source

val of_reference : 
  Tac2qexpr.reference Tac2qexpr.or_anti ->
  Tac2expr.raw_tacexpr

Sourceval of_hyp : ?loc:Loc.t -> Names.Id.t CAst.t -> Tac2expr.raw_tacexpr

id ↦ 'Control.hyp @id'

Sourceval of_exact_hyp : ?loc:Loc.t -> Names.Id.t CAst.t -> Tac2expr.raw_tacexpr

id ↦ 'Control.refine (fun () => Control.hyp @id')

Sourceval of_exact_var : ?loc:Loc.t -> Names.Id.t CAst.t -> Tac2expr.raw_tacexpr

id ↦ 'Control.refine (fun () => Control.hyp @id')

Sourceval of_dispatch : Tac2qexpr.dispatch -> Tac2expr.raw_tacexpr

Sourceval of_strategy_flag : Tac2qexpr.strategy_flag -> Tac2expr.raw_tacexpr

Sourceval of_pose : Tac2qexpr.pose -> Tac2expr.raw_tacexpr

Sourceval of_assertion : Tac2qexpr.assertion -> Tac2expr.raw_tacexpr

Sourceval of_constr_matching : Tac2qexpr.constr_matching -> Tac2expr.raw_tacexpr

Sourceval of_goal_matching : Tac2qexpr.goal_matching -> Tac2expr.raw_tacexpr

Sourceval of_format : Names.lstring -> Tac2expr.raw_tacexpr

Generic arguments

Source

val wit_pattern : 
  (Constrexpr.constr_expr, [ `uninstantiated ] Pattern.constr_pattern_r)
    Tac2dyn.Arg.tag

Sourceval wit_ident : (Names.Id.t, Names.Id.t) Tac2dyn.Arg.tag

Sourceval wit_reference : (Tac2qexpr.reference, Names.GlobRef.t) Tac2dyn.Arg.tag

Source

val wit_constr : 
  (Constrexpr.constr_expr, Glob_term.glob_constr) Tac2dyn.Arg.tag

Source

val wit_open_constr : 
  (Constrexpr.constr_expr, Glob_term.glob_constr) Tac2dyn.Arg.tag

Source

val wit_preterm : 
  (Constrexpr.constr_expr, Names.Id.Set.t * Glob_term.glob_constr)
    Tac2dyn.Arg.tag

Source

val wit_ltac1 : 
  (Names.Id.t CAst.t list * Ltac_plugin.Tacexpr.raw_tactic_expr,
    Names.Id.t list * Ltac_plugin.Tacexpr.glob_tactic_expr)
    Tac2dyn.Arg.tag

Ltac1 AST quotation, seen as a 'tactic'. Its type is unit in Ltac2.

Source

val wit_ltac1val : 
  (Names.Id.t CAst.t list * Ltac_plugin.Tacexpr.raw_tactic_expr,
    Names.Id.t list * Ltac_plugin.Tacexpr.glob_tactic_expr)
    Tac2dyn.Arg.tag

Ltac1 AST quotation, seen as a value-returning expression, with type Ltac1.t.

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac2_plugin/Ltac2_plugin/Tac2quote/index.html

Module `Ltac2_plugin.Tac2quote`Source

Generic arguments

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac2_plugin/Ltac2_plugin/Tac2quote/index.html

Module Ltac2_plugin.Tac2quoteSource

Generic arguments

Module `Ltac2_plugin.Tac2quote`Source