aboutsummaryrefslogtreecommitdiffhomepage
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 07d628171..662b7b9a2 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 b77118e1f..80e12898f 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 e2e6795f7..8df91da24 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 a4dba506d..4a9ca23f1 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 d41d23173..71d457b00 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 25162329e..68e6b7386 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 b08b7ab3c..701480fc8 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 fb3791af5..a5782298c 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 e6a50449d..e3b5e9435 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 63d5c7a57..dcf5394ea 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 14b66db36..a635285f2 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 7e3711624..88ae03057 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 03c60a8ba..1321a8598 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 2a282d221..9d37d1a2d 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 f7b137386..130d57779 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 df9f5f476..c24173abf 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 4408ab885..070d1e9c7 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 db3b60eda..017780c1f 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 341128338..3535e6c41 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 9e7d1eb5d..33c408a28 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 19ed787d1..5f4231363 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 ced535afd..1c6deae94 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 529cc737d..66668930c 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 9e6107b30..762611f75 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 d6bbfe29a..878875bd9 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.39.1) at 2024-06-26 13:33:19 +0000