Comparison with Ltac2#

The tables below map Ltac2 constructs to their equivalent in Camltac.

Types#

Type declarations#

Ltac2

OCaml

 
Ltac2 Type t := int.

type t = int

Ltac2 Type rec nat := [O | S (nat)].

type nat = O | S of nat

Ltac2 Type flag := {
  mutable used : bool
}.

type flag = { mutable used: bool }

Ltac2 Type rec tree :=
  [Node (nat, forest)]
with forest :=
  [Leaf (nat) | Cons (tree, forest)].

type tree = Node of nat * forest
and forest =
| Leaf of nat
| Cons of tree * forest

Ltac2 Type exn ::=
  [ My_error (string) ].

exception My_error of string

Ltac2 Import Type nat as n.

type n = nat

Built-in types#

Here is a mapping between Ltac2 built-in types and their OCaml counterpart.

The following types are re-exported by the Ltac2 module, e.g. Ltac2.ident is an alias for Names.Id.t:

Ltac2

OCaml

ident

Names.Id.t

evar

Evar.t

cast

Constr.cast_kind

constant

Constant.t

inductive

Ind.t

constructor

Construct.t

projection

Projection.t

pattern

Pattern.constr_pattern

constr

EConstr.t

preterm

Ltac_pretype.closed_glob_constr

binder

Name.t EConstr.binder_annot * EConstr.types

message

Pp.t

reference

GlobRef.t

err

Exninfo.iexn

iexn

Exninfo.iexn

exninfo

Exninfo.info

The other types have no alias in the Ltac2 module and are used directly through their OCaml type:

Ltac2

OCaml

'a array

'a array

int

int

string

string

char

char

exn

Ltac2.iexn

uint63

Uint63.t

float

Float64.t

pstring

Pstring.t

meta

Constr.metavariable

sort

Sorts.t

instance

EConstr.EInstance.t

Term syntax#

Ltac2

OCaml

 
fun x : nat => x

fun (x : nat) -> x

let x := y in z

let x = y in z

&x

Not implemented. Submit a PR

 
@x

{%ident| x |}

ident:(x)

{%ident| x |}

reference:(Nat.add)

Env.expand {%qualid| Nat.add |}
(* returns a list of references *)

constr:(S (S 0))

{%constr| S (S 0) |}

let x := constr:(0) in
constr:(1 + $x)

let* x = {%constr| 0 |} in
{%constr| 1 + %{x} |}

open_constr:(1 + _) (* or '(1 + _) *)

{%open_constr| 1 + _ |}

preterm:(x)

{%preterm| x |}

pat:(?n + ?m)

Not implemented. Submit a PR

Pattern matching#

Ltac2

OCaml

 
match! … with

match%rocq … with

lazy_match! … with

match%lazy … with

multi_match! … with

match%multi … with

lazy_match! constr:(S 0) with
| S ?n => n
| _ => Control.zero Not_found
end.

match%lazy {|S 0|} with
| {|S ?n|} -> return n
| _ -> Ltac2.Control.zero
  (Not_found, Exninfo.null)

match! constr:(S 0) with
| S ?n => n
| _ => Control.zero Not_found
end.

match%rocq {|S 0|} with
| {|S ?n|} -> return n
| _ -> Ltac2.Control.zero
  (Not_found, Exninfo.null)

multi_match! constr:(S 0) with
| S ?n => n
| _ => Control.zero Not_found
end.

match%multi {|S 0|} with
| {|S ?n|} -> return n
| _ -> Ltac2.Control.zero
  (Not_found, Exninfo.null)

lazy_match! goal with
| [ H : _ |- _ ] => apply H
end.

match%lazy goal with
| { h = _ }, _ ->
  let* env in
  let h = Ltac2.Control.hyp env h in
  apply [term h]

match! reverse goal with
| [ H : _ |- _ ] => apply H
end.

match%rocq reverse goal with
| { h = _ }, _ ->
  let* env in
  let h = Ltac2.Control.hyp env h in
  apply [term h]

Vernacular commands#

Ltac2

Camltac

 
Ltac2 Eval f ().

Camltac Eval ocaml:(f ()).

Ltac2 Check f ().

Camltac Check ocaml:(f ()).

Ltac2 Globalize e.

No equivalent.

 
Print Ltac2 M.

  • Camltac Check M.

Print Ltac2 Type f.

Not implemented. Submit a PR

 
Print Ltac2 Signatures.

Not implemented. Submit a PR

Definition commands#

Ltac2

Camltac

 
Ltac2 f := fun x => x.

Camltac Module M := ocaml:(
  let f x = x
).

Ltac2 Notation "foo" := ….

No equivalent.

No equivalent.

 
Camltac Load "M.ml".

No equivalent.

 
Camltac Run ocaml:(…).

Tacticals#

Ltac2

OCaml

 
let x := tac1 () in tac2

let* x = tac1 () in tac2

tac1; tac2

tac1 >> tac2

tac1 || tac2

tac1 <||> tac2

tac1 + tac2

tac1 <+> tac2

try tac

try_ tac

repeat tac

repeat tac

do 2 tac

repeat ~n:2 tac

progress tac

progress tac

first [ tac1 | tac2 ]

first [tac1; tac2]

solve [ tac1 | tac2 ]

solve [tac1; tac2]

once tac

once tac

tac > [ tac1 | tac2 ]

dispatch tac [tac1; tac2]

time tac

time tac
(* or: time ~name:"foo" tac *)

Control.timeout 5
  (fun () => tac)

timeout 5 tac

abstract tac

abstract tac