aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES8
-rw-r--r--doc/refman/RefMan-ext.tex4
-rw-r--r--parsing/g_constr.ml42
-rw-r--r--parsing/g_ltac.ml44
-rw-r--r--test-suite/bugs/closed/3249.v4
-rw-r--r--test-suite/bugs/closed/3285.v2
-rw-r--r--test-suite/bugs/closed/3286.v8
-rw-r--r--test-suite/bugs/closed/3314.v4
-rw-r--r--test-suite/bugs/closed/3330.v2
-rw-r--r--test-suite/bugs/closed/3347.v2
-rw-r--r--test-suite/bugs/closed/3354.v2
-rw-r--r--test-suite/bugs/closed/3467.v2
-rw-r--r--test-suite/bugs/closed/3487.v2
-rw-r--r--test-suite/bugs/closed/3682.v2
-rw-r--r--test-suite/bugs/closed/3684.v2
-rw-r--r--test-suite/bugs/closed/3690.v2
-rw-r--r--test-suite/bugs/closed/3881.v2
-rw-r--r--test-suite/bugs/closed/HoTT_coq_077.v2
-rw-r--r--test-suite/bugs/closed/HoTT_coq_114.v2
-rw-r--r--test-suite/bugs/opened/3248.v4
-rw-r--r--test-suite/bugs/opened/3277.v2
-rw-r--r--test-suite/bugs/opened/3278.v8
-rw-r--r--test-suite/bugs/opened/3304.v2
-rw-r--r--test-suite/bugs/opened/3459.v4
-rw-r--r--test-suite/success/polymorphism.v4
25 files changed, 45 insertions, 37 deletions
diff --git a/CHANGES b/CHANGES
index 07d6281717..662b7b9a24 100644
--- a/CHANGES
+++ b/CHANGES
@@ -10,6 +10,10 @@ Vernacular commands
introducing it.
- New command "Show id" to show goal named id.
+Specification language
+
+- Syntax "$(tactic)$" changed to "ltac: tactic".
+
Tactics
- New flag "Regular Subst Tactic" which fixes "subst" in situations where
@@ -83,6 +87,10 @@ Logic
- The VM now supports inductive types with up to 8388851 non-constant
constructors and up to 8388607 constant ones.
+Specification language
+
+- Syntax "$(tactic)$" changed to "ltac: tactic".
+
Tactics
- A script using the admit tactic can no longer be concluded by either
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index b77118e1f9..80e12898f0 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1998,7 +1998,7 @@ variables, use
\end{quote}
\subsection{Solving existential variables using tactics}
-\ttindex{\textdollar( \ldots )\textdollar}
+\ttindex{ltac:( \ldots )}
\def\expr{\textrm{\textsl{tacexpr}}}
@@ -2012,7 +2012,7 @@ binding as well as those introduced by tactic binding. The expression {\expr}
can be any tactic expression as described at section~\ref{TacticLanguage}.
\begin{coq_example*}
-Definition foo (x : nat) : nat := $( exact x )$.
+Definition foo (x : nat) : nat := ltac:(exact x).
\end{coq_example*}
This construction is useful when one wants to define complicated terms using
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index e2e6795f73..8df91da24b 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -218,7 +218,7 @@ GEXTEND Gram
CGeneralization (!@loc, Implicit, None, c)
| "`("; c = operconstr LEVEL "200"; ")" ->
CGeneralization (!@loc, Explicit, None, c)
- | "$("; tac = Tactic.tactic; ")$" ->
+ | "ltac:"; "("; tac = Tactic.tactic_expr; ")" ->
let arg = Genarg.in_gen (Genarg.rawwit Constrarg.wit_tactic) tac in
CHole (!@loc, None, IntroAnonymous, Some arg)
] ]
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index a4dba506d2..4a9ca23f15 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -134,8 +134,8 @@ GEXTEND Gram
;
(* Tactic arguments *)
tactic_arg:
- [ [ IDENT "ltac"; ":"; a = tactic_expr LEVEL "0" -> arg_of_expr a
- | IDENT "ltac"; ":"; n = natural -> TacGeneric (genarg_of_int n)
+ [ [ "ltac:"; a = tactic_expr LEVEL "0" -> arg_of_expr a
+ | "ltac:"; n = natural -> TacGeneric (genarg_of_int n)
| a = tactic_top_or_arg -> a
| r = reference -> Reference r
| c = Constr.constr -> ConstrMayEval (ConstrTerm c)
diff --git a/test-suite/bugs/closed/3249.v b/test-suite/bugs/closed/3249.v
index d41d231739..71d457b002 100644
--- a/test-suite/bugs/closed/3249.v
+++ b/test-suite/bugs/closed/3249.v
@@ -5,7 +5,7 @@ Ltac ret_and_left T :=
lazymatch eval hnf in t with
| ?a /\ ?b => constr:(proj1 T)
| forall x : ?T', @?f x =>
- constr:(fun x : T' => $(let fx := constr:(T x) in
+ constr:(fun x : T' => ltac:(let fx := constr:(T x) in
let t := ret_and_left fx in
- exact t)$)
+ exact t))
end.
diff --git a/test-suite/bugs/closed/3285.v b/test-suite/bugs/closed/3285.v
index 25162329ef..68e6b7386f 100644
--- a/test-suite/bugs/closed/3285.v
+++ b/test-suite/bugs/closed/3285.v
@@ -1,7 +1,7 @@
Goal True.
Proof.
match goal with
- | _ => let x := constr:($(fail)$) in idtac
+ | _ => let x := constr:(ltac:(fail)) in idtac
| _ => idtac
end.
Abort.
diff --git a/test-suite/bugs/closed/3286.v b/test-suite/bugs/closed/3286.v
index b08b7ab3cc..701480fc83 100644
--- a/test-suite/bugs/closed/3286.v
+++ b/test-suite/bugs/closed/3286.v
@@ -6,20 +6,20 @@ Ltac make_apply_under_binders_in lem H :=
| forall x : ?T, @?P x
=> let ret := constr:(fun x' : T =>
let Hx := H x' in
- $(let ret' := tac lem Hx in
- exact ret')$) in
+ ltac:(let ret' := tac lem Hx in
+ exact ret')) in
match eval cbv zeta in ret with
| fun x => Some (@?P x) => let P' := (eval cbv zeta in P) in
constr:(Some P')
end
- | _ => let ret := constr:($(match goal with
+ | _ => let ret := constr:(ltac:(match goal with
| _ => (let H' := fresh in
pose H as H';
apply lem in H';
exact (Some H'))
| _ => exact (@None nat)
end
- )$) in
+ )) in
let ret' := (eval cbv beta zeta in ret) in
constr:(ret')
| _ => constr:(@None nat)
diff --git a/test-suite/bugs/closed/3314.v b/test-suite/bugs/closed/3314.v
index fb3791af55..a5782298c3 100644
--- a/test-suite/bugs/closed/3314.v
+++ b/test-suite/bugs/closed/3314.v
@@ -1,9 +1,9 @@
Require Import TestSuite.admit.
Set Universe Polymorphism.
Definition Lift
-: $(let U1 := constr:(Type) in
+: ltac:(let U1 := constr:(Type) in
let U0 := constr:(Type : U1) in
- exact (U0 -> U1))$
+ exact (U0 -> U1))
:= fun T => T.
Fail Check nat:Prop. (* The command has indeed failed with message:
diff --git a/test-suite/bugs/closed/3330.v b/test-suite/bugs/closed/3330.v
index e6a50449da..e3b5e94356 100644
--- a/test-suite/bugs/closed/3330.v
+++ b/test-suite/bugs/closed/3330.v
@@ -8,7 +8,7 @@ Inductive foo : Type@{l} := bar : foo .
Section MakeEq.
Variables (a : foo@{i}) (b : foo@{j}).
- Let t := $(let ty := type of b in exact ty)$.
+ Let t := ltac:(let ty := type of b in exact ty).
Definition make_eq (x:=b) := a : t.
End MakeEq.
diff --git a/test-suite/bugs/closed/3347.v b/test-suite/bugs/closed/3347.v
index 63d5c7a57b..dcf5394eaf 100644
--- a/test-suite/bugs/closed/3347.v
+++ b/test-suite/bugs/closed/3347.v
@@ -1,7 +1,7 @@
Require Import TestSuite.admit.
(* File reduced by coq-bug-finder from original input, then from 12653 lines to 12453 lines, then from 11673 lines to 681 lines, then from 693 lines to 469 lines, then from 375 lines to 56 lines *)
Set Universe Polymorphism.
-Notation Type1 := $(let U := constr:(Type) in let gt := constr:(Set : U) in exact U)$ (only parsing).
+Notation Type1 := ltac:(let U := constr:(Type) in let gt := constr:(Set : U) in exact U) (only parsing).
Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
Inductive Unit : Type1 := tt : Unit.
Fail Check Unit : Set. (* [Check Unit : Set] should fail if [Type1] is defined correctly *)
diff --git a/test-suite/bugs/closed/3354.v b/test-suite/bugs/closed/3354.v
index 14b66db362..a635285f2c 100644
--- a/test-suite/bugs/closed/3354.v
+++ b/test-suite/bugs/closed/3354.v
@@ -1,5 +1,5 @@
Set Universe Polymorphism.
-Notation Type1 := $(let U := constr:(Type) in let gt := constr:(Set : U) in exact U)$ (only parsing).
+Notation Type1 := ltac:(let U := constr:(Type) in let gt := constr:(Set : U) in exact U) (only parsing).
Inductive Empty : Type1 := .
Fail Check Empty : Set.
(* Toplevel input, characters 15-116:
diff --git a/test-suite/bugs/closed/3467.v b/test-suite/bugs/closed/3467.v
index 7e37116249..88ae030578 100644
--- a/test-suite/bugs/closed/3467.v
+++ b/test-suite/bugs/closed/3467.v
@@ -1,5 +1,5 @@
Module foo.
- Notation x := $(exact I)$.
+ Notation x := ltac:(exact I).
End foo.
Module bar.
Include foo.
diff --git a/test-suite/bugs/closed/3487.v b/test-suite/bugs/closed/3487.v
index 03c60a8baa..1321a8598c 100644
--- a/test-suite/bugs/closed/3487.v
+++ b/test-suite/bugs/closed/3487.v
@@ -1,4 +1,4 @@
-Notation bar := $(exact I)$.
+Notation bar := ltac:(exact I).
Notation foo := bar (only parsing).
Class baz := { x : False }.
Instance: baz.
diff --git a/test-suite/bugs/closed/3682.v b/test-suite/bugs/closed/3682.v
index 2a282d221f..9d37d1a2d0 100644
--- a/test-suite/bugs/closed/3682.v
+++ b/test-suite/bugs/closed/3682.v
@@ -3,4 +3,4 @@ Class Foo.
Definition bar `{Foo} (x : Set) := Set.
Instance: Foo.
Definition bar1 := bar nat.
-Definition bar2 := bar $(admit)$.
+Definition bar2 := bar ltac:(admit).
diff --git a/test-suite/bugs/closed/3684.v b/test-suite/bugs/closed/3684.v
index f7b137386b..130d57779d 100644
--- a/test-suite/bugs/closed/3684.v
+++ b/test-suite/bugs/closed/3684.v
@@ -1,5 +1,5 @@
Require Import TestSuite.admit.
Definition foo : Set.
Proof.
- refine ($(abstract admit)$).
+ refine (ltac:(abstract admit)).
Qed.
diff --git a/test-suite/bugs/closed/3690.v b/test-suite/bugs/closed/3690.v
index df9f5f4761..c24173abf1 100644
--- a/test-suite/bugs/closed/3690.v
+++ b/test-suite/bugs/closed/3690.v
@@ -18,7 +18,7 @@ Top.8}
Top.6
Top.7
Top.8 |= *) *)
-Definition bar := $(let t := eval compute in foo in exact t)$.
+Definition bar := ltac:(let t := eval compute in foo in exact t).
Check @bar. (* bar@{Top.13 Top.14 Top.15
Top.16}
: Type@{Top.16+1}
diff --git a/test-suite/bugs/closed/3881.v b/test-suite/bugs/closed/3881.v
index 4408ab885d..070d1e9c71 100644
--- a/test-suite/bugs/closed/3881.v
+++ b/test-suite/bugs/closed/3881.v
@@ -8,7 +8,7 @@ Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
Notation "A -> B" := (forall (_ : A), B) : type_scope.
Axiom admit : forall {T}, T.
Notation "g 'o' f" := (fun x => g (f x)) (at level 40, left associativity).
-Notation "g 'o' f" := $(let g' := g in let f' := f in exact (fun x => g' (f' x)))$ (at level 40, left associativity). (* Ensure that x is not captured in [g] or [f] in case they contain holes *)
+Notation "g 'o' f" := ltac:(let g' := g in let f' := f in exact (fun x => g' (f' x))) (at level 40, left associativity). (* Ensure that x is not captured in [g] or [f] in case they contain holes *)
Inductive eq {A} (x:A) : A -> Prop := eq_refl : x = x where "x = y" := (@eq _ x y) : type_scope.
Arguments eq_refl {_ _}.
Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y := match p with eq_refl => eq_refl end.
diff --git a/test-suite/bugs/closed/HoTT_coq_077.v b/test-suite/bugs/closed/HoTT_coq_077.v
index db3b60edae..017780c1f3 100644
--- a/test-suite/bugs/closed/HoTT_coq_077.v
+++ b/test-suite/bugs/closed/HoTT_coq_077.v
@@ -30,7 +30,7 @@ Definition prod_rect' A B (P : prod A B -> Type) (u : forall (fst : A) (snd : B)
(p : prod A B) : P p
:= u (fst p) (snd p).
-Notation typeof x := ($(let T := type of x in exact T)$) (only parsing).
+Notation typeof x := (ltac:(let T := type of x in exact T)) (only parsing).
(* Check for eta *)
Check eq_refl : typeof (@prod_rect) = typeof (@prod_rect').
diff --git a/test-suite/bugs/closed/HoTT_coq_114.v b/test-suite/bugs/closed/HoTT_coq_114.v
index 341128338e..3535e6c41f 100644
--- a/test-suite/bugs/closed/HoTT_coq_114.v
+++ b/test-suite/bugs/closed/HoTT_coq_114.v
@@ -1 +1 @@
-Inductive test : $(let U := type of Type in exact U)$ := t.
+Inductive test : ltac:(let U := type of Type in exact U) := t.
diff --git a/test-suite/bugs/opened/3248.v b/test-suite/bugs/opened/3248.v
index 9e7d1eb5dd..33c408a28c 100644
--- a/test-suite/bugs/opened/3248.v
+++ b/test-suite/bugs/opened/3248.v
@@ -3,7 +3,7 @@ Ltac ret_and_left f :=
let T := type of f in
lazymatch eval hnf in T with
| ?T' -> _ =>
- let ret := constr:(fun x' : T' => $(tac (f x'))$) in
+ let ret := constr:(fun x' : T' => ltac:(tac (f x'))) in
exact ret
| ?T' => exact f
end.
@@ -12,6 +12,6 @@ Goal forall A B : Prop, forall x y : A, True.
Proof.
intros A B x y.
pose (f := fun (x y : A) => conj x y).
- pose (a := $(ret_and_left f)$).
+ pose (a := ltac:(ret_and_left f)).
Fail unify (a x y) (conj x y).
Abort.
diff --git a/test-suite/bugs/opened/3277.v b/test-suite/bugs/opened/3277.v
index 19ed787d1e..5f4231363a 100644
--- a/test-suite/bugs/opened/3277.v
+++ b/test-suite/bugs/opened/3277.v
@@ -4,4 +4,4 @@ Goal True.
evarr _.
Admitted.
Goal True.
- Fail exact $(evarr _)$. (* Error: Cannot infer this placeholder. *)
+ Fail exact ltac:(evarr _). (* Error: Cannot infer this placeholder. *)
diff --git a/test-suite/bugs/opened/3278.v b/test-suite/bugs/opened/3278.v
index ced535afd5..1c6deae94b 100644
--- a/test-suite/bugs/opened/3278.v
+++ b/test-suite/bugs/opened/3278.v
@@ -1,8 +1,8 @@
Module a.
Check let x' := _ in
- $(exact x')$.
+ ltac:(exact x').
- Notation foo x := (let x' := x in $(exact x')$).
+ Notation foo x := (let x' := x in ltac:(exact x')).
Fail Check foo _. (* Error:
Cannot infer an internal placeholder of type "Type" in environment:
@@ -12,10 +12,10 @@ x' := ?42 : ?41
End a.
Module b.
- Notation foo x := (let x' := x in let y := ($(exact I)$ : True) in I).
+ Notation foo x := (let x' := x in let y := (ltac:(exact I) : True) in I).
Notation bar x := (let x' := x in let y := (I : True) in I).
- Check let x' := _ in $(exact I)$. (* let x' := ?5 in I *)
+ Check let x' := _ in ltac:(exact I). (* let x' := ?5 in I *)
Check bar _. (* let x' := ?9 in let y := I in I *)
Fail Check foo _. (* Error:
Cannot infer an internal placeholder of type "Type" in environment:
diff --git a/test-suite/bugs/opened/3304.v b/test-suite/bugs/opened/3304.v
index 529cc737df..66668930c7 100644
--- a/test-suite/bugs/opened/3304.v
+++ b/test-suite/bugs/opened/3304.v
@@ -1,3 +1,3 @@
-Fail Notation "( x , y , .. , z )" := $(let r := constr:(prod .. (prod x y) .. z) in r)$.
+Fail Notation "( x , y , .. , z )" := ltac:(let r := constr:(prod .. (prod x y) .. z) in r).
(* The command has indeed failed with message:
=> Error: Special token .. is for use in the Notation command. *)
diff --git a/test-suite/bugs/opened/3459.v b/test-suite/bugs/opened/3459.v
index 9e6107b30a..762611f751 100644
--- a/test-suite/bugs/opened/3459.v
+++ b/test-suite/bugs/opened/3459.v
@@ -7,9 +7,9 @@ Proof.
(* This line used to fail with a Not_found up to some point, and then
to produce an ill-typed term *)
match goal with
- | [ |- context G[2] ] => let y := constr:(fun x => $(let r := constr:(@eq Set x x) in
+ | [ |- context G[2] ] => let y := constr:(fun x => ltac:(let r := constr:(@eq Set x x) in
clear x;
- exact r)$) in
+ exact r)) in
pose y
end.
(* Add extra test for typability (should not fail when bug closed) *)
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index d6bbfe29ac..878875bd92 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -242,7 +242,7 @@ Fail Check (Prop : Set).
Fail Check (Set : Set).
Check (Set : Type).
Check (Prop : Type).
-Definition setType := $(let t := type of Set in exact t)$.
+Definition setType := ltac:(let t := type of Set in exact t).
Definition foo (A : Prop) := A.
@@ -303,7 +303,7 @@ Set Printing Universes.
Axiom admit : forall A, A.
Record R := {O : Type}.
-Definition RL (x : R@{i}) : $(let u := constr:(Type@{i}:Type@{j}) in exact (R@{j}) )$ := {|O := @O x|}.
+Definition RL (x : R@{i}) : ltac:(let u := constr:(Type@{i}:Type@{j}) in exact (R@{j}) ) := {|O := @O x|}.
Definition RLRL : forall x : R, RL x = RL (RL x) := fun x => eq_refl.
Definition RLRL' : forall x : R, RL x = RL (RL x).
intros. apply eq_refl.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 06:41:43 +0000