diff options
Diffstat (limited to 'test-suite')
44 files changed, 1026 insertions, 133 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index ba591ede20..94011447d7 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -99,7 +99,7 @@ INTERACTIVE := interactive UNIT_TESTS := unit-tests VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \ - coqdoc ssr arithmetic + coqdoc ssr arithmetic ltac2 # All subsystems SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools $(UNIT_TESTS) @@ -181,6 +181,7 @@ summary: $(call summary_dir, "tools/ tests", tools); \ $(call summary_dir, "Unit tests", unit-tests); \ $(call summary_dir, "Machine arithmetic tests", arithmetic); \ + $(call summary_dir, "Ltac2 tests", ltac2); \ nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \ nb_failure=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_failure) | wc -l`; \ nb_tests=`expr $$nb_success + $$nb_failure`; \ @@ -319,7 +320,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v } > "$@" ssr: $(wildcard ssr/*.v:%.v=%.v.log) -$(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v arithmetic/*.v)): %.v.log: %.v $(PREREQUISITELOG) +$(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v arithmetic/*.v ltac2/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ opts="$(if $(findstring modules/,$<),-R modules Mods)"; \ diff --git a/test-suite/arithmetic/diveucl_21.v b/test-suite/arithmetic/diveucl_21.v index 7e12a08906..b888c97be3 100644 --- a/test-suite/arithmetic/diveucl_21.v +++ b/test-suite/arithmetic/diveucl_21.v @@ -15,3 +15,11 @@ Check (eq_refl (4611686018427387904, 1) <: diveucl_21 3 1 2 = (46116860184273879 Check (eq_refl (4611686018427387904, 1) <<: diveucl_21 3 1 2 = (4611686018427387904, 1)). Definition compute2 := Eval compute in diveucl_21 3 1 2. Check (eq_refl compute2 : (4611686018427387904, 1) = (4611686018427387904, 1)). + +Check (eq_refl : diveucl_21 1 1 0 = (0,0)). +Check (eq_refl (0,0) <: diveucl_21 1 1 0 = (0,0)). +Check (eq_refl (0,0) <<: diveucl_21 1 1 0 = (0,0)). + +Check (eq_refl : diveucl_21 9223372036854775807 0 1 = (0,0)). +Check (eq_refl (0,0) <: diveucl_21 9223372036854775807 0 1 = (0,0)). +Check (eq_refl (0,0) <<: diveucl_21 9223372036854775807 0 1 = (0,0)). diff --git a/test-suite/bugs/closed/bug_10025.v b/test-suite/bugs/closed/bug_10025.v new file mode 100644 index 0000000000..1effc771b0 --- /dev/null +++ b/test-suite/bugs/closed/bug_10025.v @@ -0,0 +1,39 @@ +Require Import Program. + +Axiom I : Type. + +Inductive S : Type := NT : I -> S. + +Axiom F : S -> Type. + +Axiom G : forall (s : S), F s -> Type. + +Section S. + +Variable init : I. +Variable my_s : F (NT init). + +Inductive foo : forall (s: S) (hole_sem: F s), Type := +| Foo : foo (NT init) my_s. + +Goal forall + (n : I) (s : F (NT n)) (ptz : foo (NT n) s) (pt : G (NT n) s) (x : unit), +match + match x with tt => tt end +with +| tt => + match + match ptz in foo x s return (forall _ : G x s, unit) with + | Foo => fun _ : G (NT init) my_s => tt + end pt + with + | tt => False + end +end. +Proof. +dependent destruction ptz. +(* Check well-typedness of goal *) +match goal with [ |- ?P ] => let t := type of P in idtac end. +Abort. + +End S. diff --git a/test-suite/bugs/closed/bug_10026.v b/test-suite/bugs/closed/bug_10026.v new file mode 100644 index 0000000000..0d3142d0f2 --- /dev/null +++ b/test-suite/bugs/closed/bug_10026.v @@ -0,0 +1,3 @@ +Require Import Coq.Lists.List. +Set Debug RAKAM. +Check fun _ => fold_right (fun A B => prod A B) unit _. diff --git a/test-suite/bugs/closed/bug_10031.v b/test-suite/bugs/closed/bug_10031.v new file mode 100644 index 0000000000..15b53de00d --- /dev/null +++ b/test-suite/bugs/closed/bug_10031.v @@ -0,0 +1,9 @@ +Require Import Int63 ZArith. + +Open Scope int63_scope. + +Goal False. +cut (let (q, r) := (0, 0) in ([|q|], [|r|]) = (9223372036854775808%Z, 0%Z)); + [discriminate| ]. +Fail (change (0, 0) with (diveucl_21 1 0 1); apply diveucl_21_spec). +Abort. diff --git a/test-suite/bugs/closed/bug_10189.v b/test-suite/bugs/closed/bug_10189.v new file mode 100644 index 0000000000..d603bff386 --- /dev/null +++ b/test-suite/bugs/closed/bug_10189.v @@ -0,0 +1,9 @@ +Definition foo : forall (x := unit) {y : nat}, nat := fun y => y. +Check foo (y := 3). (*We fail to get implicits in the type past a let-in*) +Definition foo' : forall (x : Set) {y : nat}, nat := fun _ y => y. +Check foo' unit (y := 3). (* It works with a function binder *) + +Definition bar := let f {x} : nat -> nat := fun y => x in f (x := 3). +(* Adding bar : nat -> nat gives implicits-in-term warning *) +Fail Check bar (x := 3). +(* The implicits from the type of the local definition leak to the outer term *) diff --git a/test-suite/bugs/opened/bug_3754.v b/test-suite/bugs/closed/bug_3754.v index 18820b1a4c..7031cbf132 100644 --- a/test-suite/bugs/opened/bug_3754.v +++ b/test-suite/bugs/closed/bug_3754.v @@ -281,5 +281,7 @@ Defined. (factor2 fact)). rewrite <- ap_p_pp; rewrite_moveL_Mp_p. Set Debug Tactic Unification. - Fail rewrite (concat_Ap ff2). + rewrite (concat_Ap ff2). Abort. + +End Factorization. diff --git a/test-suite/bugs/closed/bug_3890.v b/test-suite/bugs/closed/bug_3890.v new file mode 100644 index 0000000000..e1823ac54c --- /dev/null +++ b/test-suite/bugs/closed/bug_3890.v @@ -0,0 +1,12 @@ +Set Nested Proofs Allowed. + +Class Foo. +Class Bar := b : Type. + +Instance foo : Foo. + +Instance bar : Bar. +exact Type. +Defined. + +Defined. diff --git a/test-suite/bugs/closed/bug_4429.v b/test-suite/bugs/closed/bug_4429.v deleted file mode 100644 index bf0e570ab8..0000000000 --- a/test-suite/bugs/closed/bug_4429.v +++ /dev/null @@ -1,31 +0,0 @@ -Require Import Arith.Compare_dec. -Require Import Unicode.Utf8. - -Fixpoint my_nat_iter (n : nat) {A} (f : A → A) (x : A) : A := - match n with - | O => x - | S n' => f (my_nat_iter n' f x) - end. - -Definition gcd_IT_F (f : nat * nat → nat) (mn : nat * nat) : nat := - match mn with - | (0, 0) => 0 - | (0, S n') => S n' - | (S m', 0) => S m' - | (S m', S n') => - match le_gt_dec (S m') (S n') with - | left _ => f (S m', S n' - S m') - | right _ => f (S m' - S n', S n') - end - end. - -Axiom max_correct_l : ∀ m n : nat, m <= max m n. -Axiom max_correct_r : ∀ m n : nat, n <= max m n. - -Hint Resolve max_correct_l max_correct_r : arith. - -Theorem foo : ∀ p p' p'' : nat, p'' < S (max p (max p' p'')). -Proof. - intros. - Timeout 3 eauto with arith. -Qed. diff --git a/test-suite/bugs/closed/bug_4580.v b/test-suite/bugs/closed/bug_4580.v index a8a446cc9b..3f40569d61 100644 --- a/test-suite/bugs/closed/bug_4580.v +++ b/test-suite/bugs/closed/bug_4580.v @@ -2,6 +2,5 @@ Require Import Program. Class Foo (A : Type) := foo : A. -Unset Refine Instance Mode. Program Instance f1 : Foo nat := S _. Next Obligation. exact 0. Defined. diff --git a/test-suite/bugs/closed/bug_4638.v b/test-suite/bugs/closed/bug_4638.v new file mode 100644 index 0000000000..951fe5302b --- /dev/null +++ b/test-suite/bugs/closed/bug_4638.v @@ -0,0 +1,12 @@ +Set Nested Proofs Allowed. + +Class Foo. + +Goal True. + +Instance foo: Foo. +Qed. + +trivial. + +Qed. diff --git a/test-suite/bugs/closed/bug_5752.v b/test-suite/bugs/closed/bug_5752.v new file mode 100644 index 0000000000..b4218d66df --- /dev/null +++ b/test-suite/bugs/closed/bug_5752.v @@ -0,0 +1,8 @@ +Class C (A : Type) := c : A. + +Hint Mode C ! : typeclass_instances. + +Goal forall f : (forall A, C A -> C (list A)), True. +intros. + Check c. (* Loops if modes are ignored. *) +Abort. diff --git a/test-suite/bugs/closed/bug_9344.v b/test-suite/bugs/closed/bug_9344.v new file mode 100644 index 0000000000..0d44c9721a --- /dev/null +++ b/test-suite/bugs/closed/bug_9344.v @@ -0,0 +1,2 @@ +Compute _ I. +Eval native_compute in _ I. diff --git a/test-suite/bugs/closed/bug_9348.v b/test-suite/bugs/closed/bug_9348.v new file mode 100644 index 0000000000..a4673b5ffc --- /dev/null +++ b/test-suite/bugs/closed/bug_9348.v @@ -0,0 +1,3 @@ +Set Primitive Projections. +Record r {A} := R {f : A -> A}. +Compute f _ I. diff --git a/test-suite/bugs/opened/bug_3890.v b/test-suite/bugs/opened/bug_3890.v deleted file mode 100644 index 9d83743b2a..0000000000 --- a/test-suite/bugs/opened/bug_3890.v +++ /dev/null @@ -1,22 +0,0 @@ -Set Nested Proofs Allowed. - -Class Foo. -Class Bar := b : Type. - -Set Refine Instance Mode. -Instance foo : Foo := _. -Unset Refine Instance Mode. -(* 1 subgoals, subgoal 1 (ID 4) - - ============================ - Foo *) - -Instance bar : Bar. -exact Type. -Defined. -(* bar is defined *) - -About foo. -(* foo not a defined object. *) - -Fail Defined. diff --git a/test-suite/dune b/test-suite/dune index c430400ba5..cd33319fa4 100644 --- a/test-suite/dune +++ b/test-suite/dune @@ -20,6 +20,8 @@ ../dev/header.ml ../dev/tools/update-compat.py ../doc/stdlib/index-list.html.template + ; For the changelog test + ../config/coq_config.py (package coq) ; For fake_ide (package coqide-server) diff --git a/test-suite/ltac2/compat.v b/test-suite/ltac2/compat.v new file mode 100644 index 0000000000..489fa638e4 --- /dev/null +++ b/test-suite/ltac2/compat.v @@ -0,0 +1,58 @@ +Require Import Ltac2.Ltac2. + +Import Ltac2.Notations. + +(** Test calls to Ltac1 from Ltac2 *) + +Ltac2 foo () := ltac1:(discriminate). + +Goal true = false -> False. +Proof. +foo (). +Qed. + +Goal true = false -> false = true. +Proof. +intros H; ltac1:(match goal with [ H : ?P |- _ ] => rewrite H end); reflexivity. +Qed. + +Goal true = false -> false = true. +Proof. +intros H; ltac1:(rewrite H); reflexivity. +Abort. + +(** Variables do not cross the compatibility layer boundary. *) +Fail Ltac2 bar nay := ltac1:(discriminate nay). + +Fail Ltac2 pose1 (v : constr) := + ltac1:(pose $v). + +(** Test calls to Ltac2 from Ltac1 *) + +Set Default Proof Mode "Classic". + +Ltac foo := ltac2:(foo ()). + +Goal true = false -> False. +Proof. +ltac2:(foo ()). +Qed. + +Goal true = false -> False. +Proof. +foo. +Qed. + +(** Variables do not cross the compatibility layer boundary. *) +Fail Ltac bar x := ltac2:(foo x). + +Ltac mytac tac := idtac "wow". + +Goal True. +Proof. +(** Fails because quotation is evaluated eagerly *) +Fail mytac ltac2:(fail). +(** One has to thunk thanks to the idtac trick *) +let t := idtac; ltac2:(fail) in mytac t. +constructor. +Qed. diff --git a/test-suite/ltac2/errors.v b/test-suite/ltac2/errors.v new file mode 100644 index 0000000000..c677f6af5d --- /dev/null +++ b/test-suite/ltac2/errors.v @@ -0,0 +1,12 @@ +Require Import Ltac2.Ltac2. + +Goal True. +Proof. +let x := Control.plus + (fun () => let _ := constr:(nat -> 0) in 0) + (fun e => match e with Not_found => 1 | _ => 2 end) in +match Int.equal x 2 with +| true => () +| false => Control.throw (Tactic_failure None) +end. +Abort. diff --git a/test-suite/ltac2/example1.v b/test-suite/ltac2/example1.v new file mode 100644 index 0000000000..023791050f --- /dev/null +++ b/test-suite/ltac2/example1.v @@ -0,0 +1,27 @@ +Require Import Ltac2.Ltac2. + +Import Ltac2.Control. + +(** Alternative implementation of the hyp primitive *) +Ltac2 get_hyp_by_name x := + let h := hyps () in + let rec find x l := match l with + | [] => zero Not_found + | p :: l => + match p with + | (id, _, t) => + match Ident.equal x id with + | true => t + | false => find x l + end + end + end in + find x h. + +Print Ltac2 get_hyp_by_name. + +Goal forall n m, n + m = 0 -> n = 0. +Proof. +refine (fun () => '(fun n m H => _)). +let t := get_hyp_by_name @H in Message.print (Message.of_constr t). +Abort. diff --git a/test-suite/ltac2/example2.v b/test-suite/ltac2/example2.v new file mode 100644 index 0000000000..c953d25061 --- /dev/null +++ b/test-suite/ltac2/example2.v @@ -0,0 +1,281 @@ +Require Import Ltac2.Ltac2. + +Import Ltac2.Notations. + +Set Default Goal Selector "all". + +Goal exists n, n = 0. +Proof. +split with (x := 0). +reflexivity. +Qed. + +Goal exists n, n = 0. +Proof. +split with 0. +split. +Qed. + +Goal exists n, n = 0. +Proof. +let myvar := Std.NamedHyp @x in split with ($myvar := 0). +split. +Qed. + +Goal (forall n : nat, n = 0 -> False) -> True. +Proof. +intros H. +eelim &H. +split. +Qed. + +Goal (forall n : nat, n = 0 -> False) -> True. +Proof. +intros H. +elim &H with 0. +split. +Qed. + +Goal forall (P : nat -> Prop), (forall n m, n = m -> P n) -> P 0. +Proof. +intros P H. +Fail apply &H. +apply &H with (m := 0). +split. +Qed. + +Goal forall (P : nat -> Prop), (forall n m, n = m -> P n) -> (0 = 1) -> P 0. +Proof. +intros P H e. +apply &H with (m := 1) in e. +exact e. +Qed. + +Goal forall (P : nat -> Prop), (forall n m, n = m -> P n) -> P 0. +Proof. +intros P H. +eapply &H. +split. +Qed. + +Goal exists n, n = 0. +Proof. +Fail constructor 1. +constructor 1 with (x := 0). +split. +Qed. + +Goal exists n, n = 0. +Proof. +econstructor 1. +split. +Qed. + +Goal forall n, 0 + n = n. +Proof. +intros n. +induction &n as [|n] using nat_rect; split. +Qed. + +Goal forall n, 0 + n = n. +Proof. +intros n. +let n := @X in +let q := Std.NamedHyp @P in +induction &n as [|$n] using nat_rect with ($q := fun m => 0 + m = m); split. +Qed. + +Goal forall n, 0 + n = n. +Proof. +intros n. +destruct &n as [|n] using nat_rect; split. +Qed. + +Goal forall n, 0 + n = n. +Proof. +intros n. +let n := @X in +let q := Std.NamedHyp @P in +destruct &n as [|$n] using nat_rect with ($q := fun m => 0 + m = m); split. +Qed. + +Goal forall b1 b2, andb b1 b2 = andb b2 b1. +Proof. +intros b1 b2. +destruct &b1 as [|], &b2 as [|]; split. +Qed. + +Goal forall n m, n = 0 -> n + m = m. +Proof. +intros n m Hn. +rewrite &Hn; split. +Qed. + +Goal forall n m p, n = m -> p = m -> 0 = n -> p = 0. +Proof. +intros n m p He He' Hn. +rewrite &He, <- &He' in Hn. +rewrite &Hn. +split. +Qed. + +Goal forall n m, (m = n -> n = m) -> m = n -> n = 0 -> m = 0. +Proof. +intros n m He He' He''. +rewrite <- &He by assumption. +Control.refine (fun () => &He''). +Qed. + +Goal forall n (r := if true then n else 0), r = n. +Proof. +intros n r. +hnf in r. +split. +Qed. + +Goal 1 = 0 -> 0 = 0. +Proof. +intros H. +pattern 0 at 1. +let occ := 2 in pattern 1 at 1, 0 at $occ in H. +reflexivity. +Qed. + +Goal 1 + 1 = 2. +Proof. +vm_compute. +reflexivity. +Qed. + +Goal 1 + 1 = 2. +Proof. +native_compute. +reflexivity. +Qed. + +Goal 1 + 1 = 2 - 0 -> True. +Proof. +intros H. +vm_compute plus in H. +reflexivity. +Qed. + +Goal 1 = 0 -> True /\ True. +Proof. +intros H. +split; fold (1 + 0) (1 + 0) in H. +reflexivity. +Qed. + +Goal 1 + 1 = 2. +Proof. +cbv [ Nat.add ]. +reflexivity. +Qed. + +Goal 1 + 1 = 2. +Proof. +let x := reference:(Nat.add) in +cbn beta iota delta [ $x ]. +reflexivity. +Qed. + +Goal 1 + 1 = 2. +Proof. +simpl beta. +reflexivity. +Qed. + +Goal 1 + 1 = 2. +Proof. +lazy. +reflexivity. +Qed. + +Goal let x := 1 + 1 - 1 in x = x. +Proof. +intros x. +unfold &x at 1. +let x := reference:(Nat.sub) in unfold Nat.add, $x in x. +reflexivity. +Qed. + +Goal exists x y : nat, x = y. +Proof. +exists 0, 0; reflexivity. +Qed. + +Goal exists x y : nat, x = y. +Proof. +eexists _, 0; reflexivity. +Qed. + +Goal exists x y : nat, x = y. +Proof. +refine '(let x := 0 in _). +eexists; exists &x; reflexivity. +Qed. + +Goal True. +Proof. +pose (X := True). +constructor. +Qed. + +Goal True. +Proof. +pose True as X. +constructor. +Qed. + +Goal True. +Proof. +let x := @foo in +set ($x := True) in * |-. +constructor. +Qed. + +Goal 0 = 0. +Proof. +remember 0 as n eqn: foo at 1. +rewrite foo. +reflexivity. +Qed. + +Goal True. +Proof. +assert (H := 0 + 0). +constructor. +Qed. + +Goal True. +Proof. +assert (exists n, n = 0) as [n Hn]. ++ exists 0; reflexivity. ++ exact I. +Qed. + +Goal True -> True. +Proof. +assert (H : 0 + 0 = 0) by reflexivity. +intros x; exact x. +Qed. + +Goal 1 + 1 = 2. +Proof. +change (?a + 1 = 2) with (2 = $a + 1). +reflexivity. +Qed. + +Goal (forall n, n = 0 -> False) -> False. +Proof. +intros H. +specialize (H 0 eq_refl). +destruct H. +Qed. + +Goal (forall n, n = 0 -> False) -> False. +Proof. +intros H. +specialize (H 0 eq_refl) as []. +Qed. diff --git a/test-suite/ltac2/matching.v b/test-suite/ltac2/matching.v new file mode 100644 index 0000000000..4338cbd32f --- /dev/null +++ b/test-suite/ltac2/matching.v @@ -0,0 +1,71 @@ +Require Import Ltac2.Ltac2 Ltac2.Notations. + +Ltac2 Type exn ::= [ Nope ]. + +Ltac2 check_id id id' := match Ident.equal id id' with +| true => () +| false => Control.throw Nope +end. + +Goal True -> False. +Proof. +Fail +let b := { contents := true } in +let f c := + match b.(contents) with + | true => Message.print (Message.of_constr c); b.(contents) := false; fail + | false => () + end +in +(** This fails because the matching is not allowed to backtrack once + it commits to a branch*) +lazy_match! '(nat -> bool) with context [?a] => f a end. +lazy_match! Control.goal () with ?a -> ?b => Message.print (Message.of_constr b) end. + +(** This one works by taking the second match context, i.e. ?a := nat *) +let b := { contents := true } in +let f c := + match b.(contents) with + | true => b.(contents) := false; fail + | false => Message.print (Message.of_constr c) + end +in +match! '(nat -> bool) with context [?a] => f a end. +Abort. + +Goal forall (i j : unit) (x y : nat) (b : bool), True. +Proof. +Fail match! goal with +| [ h : ?t, h' : ?t |- _ ] => () +end. +intros i j x y b. +match! goal with +| [ h : ?t, h' : ?t |- _ ] => + check_id h @x; + check_id h' @y +end. +match! reverse goal with +| [ h : ?t, h' : ?t |- _ ] => + check_id h @j; + check_id h' @i +end. +Abort. + +(* Check #79 *) +Goal 2 = 3. + Control.plus + (fun () + => lazy_match! goal with + | [ |- 2 = 3 ] => Control.zero (Tactic_failure None) + | [ |- 2 = _ ] => Control.zero (Tactic_failure (Some (Message.of_string "should not be printed"))) + end) + (fun e + => match e with + | Tactic_failure c + => match c with + | None => () + | _ => Control.zero e + end + | e => Control.zero e + end). +Abort. diff --git a/test-suite/ltac2/quot.v b/test-suite/ltac2/quot.v new file mode 100644 index 0000000000..624c4ad0c1 --- /dev/null +++ b/test-suite/ltac2/quot.v @@ -0,0 +1,26 @@ +Require Import Ltac2.Ltac2. + +(** Test for quotations *) + +Ltac2 ref0 () := reference:(&x). +Ltac2 ref1 () := reference:(nat). +Ltac2 ref2 () := reference:(Datatypes.nat). +Fail Ltac2 ref () := reference:(i_certainly_dont_exist). +Fail Ltac2 ref () := reference:(And.Me.neither). + +Goal True. +Proof. +let x := constr:(I) in +let y := constr:((fun z => z) $x) in +Control.refine (fun _ => y). +Qed. + +Goal True. +Proof. +(** Here, Ltac2 should not put its variables in the same environment as + Ltac1 otherwise the second binding fails as x is bound but not an + ident. *) +let x := constr:(I) in +let y := constr:((fun x => x) $x) in +Control.refine (fun _ => y). +Qed. diff --git a/test-suite/ltac2/rebind.v b/test-suite/ltac2/rebind.v new file mode 100644 index 0000000000..e1c20a2059 --- /dev/null +++ b/test-suite/ltac2/rebind.v @@ -0,0 +1,34 @@ +Require Import Ltac2.Ltac2 Ltac2.Notations. + +Ltac2 mutable foo () := constructor. + +Goal True. +Proof. +foo (). +Qed. + +Ltac2 Set foo := fun _ => fail. + +Goal True. +Proof. +Fail foo (). +constructor. +Qed. + +(** Not the right type *) +Fail Ltac2 Set foo := 0. + +Ltac2 bar () := (). + +(** Cannot redefine non-mutable tactics *) +Fail Ltac2 Set bar := fun _ => (). + +(** Subtype check *) + +Ltac2 mutable rec f x := f x. + +Fail Ltac2 Set f := fun x => x. + +Ltac2 mutable g x := x. + +Ltac2 Set g := f. diff --git a/test-suite/ltac2/stuff/ltac2.v b/test-suite/ltac2/stuff/ltac2.v new file mode 100644 index 0000000000..370bc70d15 --- /dev/null +++ b/test-suite/ltac2/stuff/ltac2.v @@ -0,0 +1,143 @@ +Require Import Ltac2.Ltac2. + +Ltac2 foo (_ : int) := + let f (x : int) := x in + let _ := f 0 in + f 1. + +Print Ltac2 foo. + +Import Control. + +Ltac2 exact x := refine (fun () => x). + +Print Ltac2 refine. +Print Ltac2 exact. + +Ltac2 foo' () := ident:(bla). + +Print Ltac2 foo'. + +Ltac2 bar x h := match x with +| None => constr:(fun H => ltac2:(exact (hyp ident:(H))) -> nat) +| Some x => x +end. + +Print Ltac2 bar. + +Ltac2 qux := Some 0. + +Print Ltac2 qux. + +Ltac2 Type foo := [ Foo (int) ]. + +Fail Ltac2 qux0 := Foo None. + +Ltac2 Type 'a ref := { mutable contents : 'a }. + +Fail Ltac2 qux0 := { contents := None }. +Ltac2 foo0 () := { contents := None }. + +Print Ltac2 foo0. + +Ltac2 qux0 x := x.(contents). +Ltac2 qux1 x := x.(contents) := x.(contents). + +Ltac2 qux2 := ([1;2], true). + +Print Ltac2 qux0. +Print Ltac2 qux1. +Print Ltac2 qux2. + +Import Control. + +Ltac2 qux3 x := constr:(nat -> ltac2:(refine (fun () => hyp x))). + +Print Ltac2 qux3. + +Ltac2 Type rec nat := [ O | S (nat) ]. + +Ltac2 message_of_nat n := +let rec aux n := +match n with +| O => Message.of_string "O" +| S n => Message.concat (Message.of_string "S") (aux n) +end in aux n. + +Print Ltac2 message_of_nat. + +Ltac2 numgoals () := + let r := { contents := O } in + enter (fun () => r.(contents) := S (r.(contents))); + r.(contents). + +Print Ltac2 numgoals. + +Goal True /\ False. +Proof. +let n := numgoals () in Message.print (message_of_nat n). +refine (fun () => open_constr:((fun x => conj _ _) 0)); (). +let n := numgoals () in Message.print (message_of_nat n). + +Fail (hyp ident:(x)). +Fail (enter (fun () => hyp ident:(There_is_no_spoon); ())). + +enter (fun () => Message.print (Message.of_string "foo")). + +enter (fun () => Message.print (Message.of_constr (goal ()))). +Fail enter (fun () => Message.print (Message.of_constr (qux3 ident:(x)))). +enter (fun () => plus (fun () => constr:(_); ()) (fun _ => ())). +plus + (fun () => enter (fun () => let x := ident:(foo) in let _ := hyp x in ())) (fun _ => Message.print (Message.of_string "failed")). +let x := { contents := 0 } in +let x := x.(contents) := x.(contents) in x. +Abort. + +Ltac2 Type exn ::= [ Foo ]. + +Goal True. +Proof. +plus (fun () => zero Foo) (fun _ => ()). +Abort. + +Ltac2 Type exn ::= [ Bar (string) ]. + +Goal True. +Proof. +Fail zero (Bar "lol"). +Abort. + +Ltac2 Notation "refine!" c(thunk(constr)) := refine c. + +Goal True. +Proof. +refine! I. +Abort. + +Goal True. +Proof. +let x () := plus (fun () => 0) (fun _ => 1) in +match case x with +| Val x => + match x with + | (x, k) => Message.print (Message.of_int (k Not_found)) + end +| Err x => Message.print (Message.of_string "Err") +end. +Abort. + +Goal (forall n : nat, n = 0 -> False) -> True. +Proof. +refine (fun () => '(fun H => _)). +Std.case true (hyp @H, Std.ExplicitBindings [Std.NamedHyp @n, '0]). +refine (fun () => 'eq_refl). +Qed. + +Goal forall x, 1 + x = x + 1. +Proof. +refine (fun () => '(fun x => _)). +Std.cbv { + Std.rBeta := true; Std.rMatch := true; Std.rFix := true; Std.rCofix := true; + Std.rZeta := true; Std.rDelta := true; Std.rConst := []; +} { Std.on_hyps := None; Std.on_concl := Std.AllOccurrences }. +Abort. diff --git a/test-suite/ltac2/tacticals.v b/test-suite/ltac2/tacticals.v new file mode 100644 index 0000000000..1a2fbcbb37 --- /dev/null +++ b/test-suite/ltac2/tacticals.v @@ -0,0 +1,34 @@ +Require Import Ltac2.Ltac2. + +Import Ltac2.Notations. + +Goal True. +Proof. +Fail fail. +Fail solve [ () ]. +try fail. +repeat fail. +repeat (). +solve [ constructor ]. +Qed. + +Goal True. +Proof. +first [ + Message.print (Message.of_string "Yay"); fail +| constructor +| Message.print (Message.of_string "I won't be printed") +]. +Qed. + +Goal True /\ True. +Proof. +Fail split > [ split | |]. +split > [split | split]. +Qed. + +Goal True /\ (True -> True) /\ True. +Proof. +split > [ | split] > [split | .. | split]. +intros H; refine &H. +Qed. diff --git a/test-suite/ltac2/typing.v b/test-suite/ltac2/typing.v new file mode 100644 index 0000000000..9f18292716 --- /dev/null +++ b/test-suite/ltac2/typing.v @@ -0,0 +1,72 @@ +Require Import Ltac2.Ltac2. + +(** Ltac2 is typed à la ML. *) + +Ltac2 test0 n := Int.add n 1. + +Print Ltac2 test0. + +Ltac2 test1 () := test0 0. + +Print Ltac2 test1. + +Fail Ltac2 test2 () := test0 true. + +Fail Ltac2 test2 () := test0 0 0. + +Ltac2 test3 f x := x, (f x, x). + +Print Ltac2 test3. + +(** Polymorphism *) + +Ltac2 rec list_length l := +match l with +| [] => 0 +| x :: l => Int.add 1 (list_length l) +end. + +Print Ltac2 list_length. + +(** Pattern-matching *) + +Ltac2 ifb b f g := match b with +| true => f () +| false => g () +end. + +Print Ltac2 ifb. + +Ltac2 if_not_found e f g := match e with +| Not_found => f () +| _ => g () +end. + +Fail Ltac2 ifb' b f g := match b with +| true => f () +end. + +Fail Ltac2 if_not_found' e f g := match e with +| Not_found => f () +end. + +(** Reimplementing 'do'. Return value of the function useless. *) + +Ltac2 rec do n tac := match Int.equal n 0 with +| true => () +| false => tac (); do (Int.sub n 1) tac +end. + +Print Ltac2 do. + +(** Non-function pure values are OK. *) + +Ltac2 tuple0 := ([1; 2], true, (fun () => "yay")). + +Print Ltac2 tuple0. + +(** Impure values are not. *) + +Fail Ltac2 not_a_value := { contents := 0 }. +Fail Ltac2 not_a_value := "nope". +Fail Ltac2 not_a_value := list_length []. diff --git a/test-suite/misc/changelog.sh b/test-suite/misc/changelog.sh new file mode 100755 index 0000000000..8b4a49e577 --- /dev/null +++ b/test-suite/misc/changelog.sh @@ -0,0 +1,18 @@ +#!/bin/sh + +while read line; do + if [ "$line" = "is_a_released_version = False" ]; then + echo "This is not a released version: nothing to test." + exit 0 + fi +done < ../config/coq_config.py + +for d in ../doc/changelog/*; do + if [ -d "$d" ]; then + if [ "$(ls $d/*.rst | wc -l)" != "1" ]; then + echo "Fatal: unreleased changelog entries remain in ${d#../}/" + echo "Include them in doc/sphinx/changes.rst and remove them from doc/changelog/" + exit 1 + fi + fi +done diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index 7074ad2d41..3c1e27ba9d 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -27,7 +27,7 @@ Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] The reduction tactics unfold Nat.sub when the 1st and - 2nd arguments evaluate to a constructor and when applied to 2 arguments + 2nd arguments evaluate to a constructor and when applied to 2 arguments Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat @@ -35,7 +35,7 @@ Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] The reduction tactics unfold Nat.sub when the 1st and - 2nd arguments evaluate to a constructor + 2nd arguments evaluate to a constructor Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub pf : @@ -54,7 +54,7 @@ fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C fcomp is not universe polymorphic Arguments A, B, C are implicit and maximally inserted Argument scopes are [type_scope type_scope type_scope _ _ _] -The reduction tactics unfold fcomp when applied to 6 arguments +The reduction tactics unfold fcomp when applied to 6 arguments fcomp is transparent Expands to: Constant Arguments.fcomp volatile : nat -> nat @@ -75,7 +75,7 @@ f : T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic Argument scopes are [_ _ nat_scope _ nat_scope] The reduction tactics unfold f when the 3rd, 4th and - 5th arguments evaluate to a constructor + 5th arguments evaluate to a constructor f is transparent Expands to: Constant Arguments.S1.S2.f f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat @@ -84,7 +84,7 @@ f is not universe polymorphic Argument T2 is implicit Argument scopes are [type_scope _ _ nat_scope _ nat_scope] The reduction tactics unfold f when the 4th, 5th and - 6th arguments evaluate to a constructor + 6th arguments evaluate to a constructor f is transparent Expands to: Constant Arguments.S1.f f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat @@ -93,7 +93,7 @@ f is not universe polymorphic Arguments T1, T2 are implicit Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope] The reduction tactics unfold f when the 5th, 6th and - 7th arguments evaluate to a constructor + 7th arguments evaluate to a constructor f is transparent Expands to: Constant Arguments.f = forall v : unit, f 0 0 5 v 3 = 2 @@ -104,7 +104,7 @@ f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic The reduction tactics unfold f when the 5th, 6th and - 7th arguments evaluate to a constructor + 7th arguments evaluate to a constructor f is transparent Expands to: Constant Arguments.f forall w : r, w 3 true = tt @@ -115,3 +115,13 @@ w 3 true = tt : Prop The command has indeed failed with message: Extra arguments: _, _. +volatilematch : nat -> nat + +volatilematch is not universe polymorphic +Argument scope is [nat_scope] +The reduction tactics always unfold volatilematch + but avoid exposing match constructs +volatilematch is transparent +Expands to: Constant Arguments.volatilematch + = fun n : nat => volatilematch n + : nat -> nat diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v index 844f96aaa1..b909f1b64c 100644 --- a/test-suite/output/Arguments.v +++ b/test-suite/output/Arguments.v @@ -55,3 +55,12 @@ Arguments w x%F y%B : extra scopes. Check (w $ $ = tt). Fail Arguments w _%F _%B. +Definition volatilematch (n : nat) := + match n with + | O => O + | S p => p + end. + +Arguments volatilematch / n : simpl nomatch. +About volatilematch. +Eval simpl in fun n => volatilematch n. diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 3f0717666c..65c902202d 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -62,7 +62,7 @@ Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] The reduction tactics unfold myplus when the 2nd and - 3rd arguments evaluate to a constructor + 3rd arguments evaluate to a constructor myplus is transparent Expands to: Constant Arguments_renaming.Test1.myplus @myplus @@ -101,7 +101,7 @@ Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] The reduction tactics unfold myplus when the 2nd and - 3rd arguments evaluate to a constructor + 3rd arguments evaluate to a constructor myplus is transparent Expands to: Constant Arguments_renaming.myplus @myplus diff --git a/test-suite/output/Error_msg_diffs.v b/test-suite/output/Error_msg_diffs.v index 11c766b210..a26e683398 100644 --- a/test-suite/output/Error_msg_diffs.v +++ b/test-suite/output/Error_msg_diffs.v @@ -1,4 +1,4 @@ -(* coq-prog-args: ("-color" "on" "-async-proofs" "off") *) +(* coq-prog-args: ("-color" "on" "-diffs" "on" "-async-proofs" "off") *) (* Re: -async-proofs off, see https://github.com/coq/coq/issues/9671 *) (* Shows diffs in an error message for an "Unable to unify" error *) Require Import Arith List Bool. diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 9d972a68f7..c1b9a2b1c6 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -1,5 +1,15 @@ [< 0 > + < 1 > * < 2 >] : nat +Entry constr:myconstr is +[ "6" RIGHTA + [ ] +| "5" RIGHTA + [ SELF; "+"; NEXT ] +| "4" RIGHTA + [ SELF; "*"; NEXT ] +| "3" RIGHTA + [ "<"; constr:operconstr LEVEL "10"; ">" ] ] + [< b > + < b > * < 2 >] : nat [<< # 0 >>] diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 81c64418cb..d1063bfd04 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -9,6 +9,7 @@ Notation "x + y" := (Nat.add x y) (in custom myconstr at level 5). Notation "x * y" := (Nat.mul x y) (in custom myconstr at level 4). Notation "< x >" := x (in custom myconstr at level 3, x constr at level 10). Check [ < 0 > + < 1 > * < 2 >]. +Print Custom Grammar myconstr. Axiom a : nat. Notation b := a. diff --git a/test-suite/output/Quote.out b/test-suite/output/Quote.out deleted file mode 100644 index 998eb37cc8..0000000000 --- a/test-suite/output/Quote.out +++ /dev/null @@ -1,24 +0,0 @@ -(interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx)) -(interp_f (Node_vm B (Empty_vm Prop) (Empty_vm Prop)) - (f_and (f_const A) - (f_and (f_or (f_atom End_idx) (f_const A)) - (f_or (f_const A) (f_not (f_atom End_idx)))))) -1 subgoal - - H : interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx) \/ - B - ============================ - interp_f - (Node_vm B (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (Empty_vm Prop)) - (f_and (f_atom (Left_idx End_idx)) - (f_and (f_or (f_atom End_idx) (f_atom (Left_idx End_idx))) - (f_or (f_atom (Left_idx End_idx)) (f_not (f_atom End_idx))))) -1 subgoal - - H : interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx) \/ - B - ============================ - interp_f (Node_vm B (Empty_vm Prop) (Empty_vm Prop)) - (f_and (f_const A) - (f_and (f_or (f_atom End_idx) (f_const A)) - (f_or (f_const A) (f_not (f_atom End_idx))))) diff --git a/test-suite/output/bug_9370.out b/test-suite/output/bug_9370.out new file mode 100644 index 0000000000..0ff151c8b4 --- /dev/null +++ b/test-suite/output/bug_9370.out @@ -0,0 +1,12 @@ +1 subgoal + + ============================ + 1 = 1 +1 subgoal + + ============================ + 1 = 1 +1 subgoal + + ============================ + 1 = 1 diff --git a/test-suite/output/bug_9370.v b/test-suite/output/bug_9370.v new file mode 100644 index 0000000000..a7f4b7c23e --- /dev/null +++ b/test-suite/output/bug_9370.v @@ -0,0 +1,12 @@ +Require Import Reals. +Open Scope R_scope. +Goal 1/1=1. +Proof. + field_simplify (1/1). +Show. + field_simplify. +Show. + field_simplify. +Show. + reflexivity. +Qed. diff --git a/test-suite/prerequisite/ssr_mini_mathcomp.v b/test-suite/prerequisite/ssr_mini_mathcomp.v index ca360f65a7..6fc630056c 100644 --- a/test-suite/prerequisite/ssr_mini_mathcomp.v +++ b/test-suite/prerequisite/ssr_mini_mathcomp.v @@ -634,9 +634,9 @@ Fixpoint mem_seq (s : seq T) := Definition eqseq_class := seq T. Identity Coercion seq_of_eqseq : eqseq_class >-> seq. -Coercion pred_of_eq_seq (s : eqseq_class) : pred_class := [eta mem_seq s]. +Coercion pred_of_eq_seq (s : eqseq_class) : {pred T} := [eta mem_seq s]. -Canonical seq_predType := @mkPredType T (seq T) pred_of_eq_seq. +Canonical seq_predType := @PredType T (seq T) pred_of_eq_seq. Fixpoint uniq s := if s is x :: s' then (x \notin s') && uniq s' else true. diff --git a/test-suite/ssr/nonPropType.v b/test-suite/ssr/nonPropType.v new file mode 100644 index 0000000000..bcdc907b38 --- /dev/null +++ b/test-suite/ssr/nonPropType.v @@ -0,0 +1,23 @@ +Require Import ssreflect. + +(** Test the nonPropType interface and its application to prevent unwanted + instantiations in views. **) + +Lemma raw_flip {T} (x y : T) : x = y -> y = x. Proof. by []. Qed. +Lemma flip {T : nonPropType} (x y : T) : x = y -> y = x. Proof. by []. Qed. + +Lemma testSet : true = false -> True. +Proof. +Fail move/raw_flip. +have flip_true := @flip _ true. +(* flip_true : forall y : notProp bool, x = y -> y = x *) +simpl in flip_true. +(* flip_true : forall y : bool, x = y -> y = x *) +by move/flip. +Qed. + +Lemma override (t1 t2 : True) : t1 = t2 -> True. +Proof. +Fail move/flip. +by move/(@flip (notProp True)). +Qed. diff --git a/test-suite/ssr/predRewrite.v b/test-suite/ssr/predRewrite.v new file mode 100644 index 0000000000..2ad762ccf1 --- /dev/null +++ b/test-suite/ssr/predRewrite.v @@ -0,0 +1,28 @@ +Require Import ssreflect ssrfun ssrbool. + +(** Test the various idioms that control rewriting in boolean predicate. **) + +Definition simpl_P := [pred a | ~~ a]. +Definition nosimpl_P : pred bool := [pred a | ~~ a]. +Definition coll_P : collective_pred bool := [pred a | ~~ a]. +Definition appl_P : applicative_pred bool := [pred a | ~~ a]. +Definition can_appl_P : pred bool := [pred a | ~~ a]. +Canonical register_can_appl_P := ApplicativePred can_appl_P. +Ltac see_neg := (let x := fresh "x" in set x := {-}(~~ _); clear x). + +Lemma test_pred_rewrite (f := false) : True. +Proof. +have _: f \in simpl_P by rewrite inE; see_neg. +have _ a: simpl_P (a && f) by simpl; see_neg; rewrite andbF. +have _ a: simpl_P (a && f) by rewrite inE; see_neg; rewrite andbF. +have _: f \in nosimpl_P by rewrite inE; see_neg. +have _: nosimpl_P f. simpl. Fail see_neg. Fail rewrite inE. done. +have _: f \in coll_P. Fail rewrite inE. by rewrite in_collective; see_neg. +have _: f \in appl_P. + rewrite inE. Fail see_neg. Fail rewrite inE. simpl. Fail see_neg. + Fail rewrite app_predE. done. +have _: f \in can_appl_P. + rewrite inE. Fail see_neg. Fail rewrite inE. simpl. Fail see_neg. + by rewrite app_predE in_simpl; see_neg. +done. +Qed. diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index 2533a39cc4..d047f7560e 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -151,8 +151,8 @@ Module M16. Local Notation "##" := 0 (in custom foo2). (* Test Print Grammar *) - Print Grammar foo. - Print Grammar foo2. + Print Custom Grammar foo. + Print Custom Grammar foo2. End M16. (* Example showing the need for strong evaluation of diff --git a/test-suite/success/ROmega3.v b/test-suite/success/ROmega3.v deleted file mode 100644 index ef9cb17b4b..0000000000 --- a/test-suite/success/ROmega3.v +++ /dev/null @@ -1,35 +0,0 @@ - -Require Import ZArith Lia. -Local Open Scope Z_scope. - -(** Benchmark provided by Chantal Keller, that romega used to - solve far too slowly (compared to omega or lia). *) - -(* In Coq 8.9 (end of 2018), the `romega` tactics are deprecated. - The tests in this file remain but now call the `lia` tactic. *) - - -Parameter v4 : Z. -Parameter v3 : Z. -Parameter o4 : Z. -Parameter s5 : Z. -Parameter v2 : Z. -Parameter o5 : Z. -Parameter s6 : Z. -Parameter v1 : Z. -Parameter o6 : Z. -Parameter s7 : Z. -Parameter v0 : Z. -Parameter o7 : Z. - -Lemma lemma_5833 : - ~ 16 * v4 + (8 * v3 + (-8192 * o4 + (-4096 * s5 + (4 * v2 + - (-4096 * o5 + (-2048 * s6 + (2 * v1 + (-2048 * o6 + - (-1024 * s7 + (v0 + -1024 * o7)))))))))) >= 8192 -\/ - 16 * v4 + (8 * v3 + (-8192 * o4 + (-4096 * s5 + (4 * v2 + - (-4096 * o5 + (-2048 * s6 + (2 * v1 + (-2048 * o6 + - (-1024 * s7 + (v0 + -1024 * o7)))))))))) >= 1024. -Proof. -Timeout 1 lia. (* should take a few milliseconds, not seconds *) -Timeout 1 Qed. (* ditto *) diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index 3888cafed3..736d05fefc 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -198,9 +198,7 @@ Module UniqueInstances. for it. *) Set Typeclasses Unique Instances. Class Eq (A : Type) : Set. - Set Refine Instance Mode. - Instance eqa : Eq nat := _. constructor. Qed. - Unset Refine Instance Mode. + Instance eqa : Eq nat. Qed. Instance eqb : Eq nat := {}. Class Foo (A : Type) (e : Eq A) : Set. Instance fooa : Foo _ eqa := {}. diff --git a/test-suite/success/attribute_syntax.v b/test-suite/success/attribute_syntax.v index f4f59a3c16..4717759dec 100644 --- a/test-suite/success/attribute_syntax.v +++ b/test-suite/success/attribute_syntax.v @@ -20,6 +20,10 @@ Check ι _ ι. Fixpoint f (n: nat) {wf lt n} : nat := _. Reset f. +#[program(true)] +Fixpoint f (n: nat) {wf lt n} : nat := _. +Reset f. + #[deprecated(since="8.9.0")] Ltac foo := foo. diff --git a/test-suite/success/change.v b/test-suite/success/change.v index a9821b027f..2f676cf9ad 100644 --- a/test-suite/success/change.v +++ b/test-suite/success/change.v @@ -68,3 +68,16 @@ eassumption. match goal with |- ?x=1 => change (x=1) with (0+x=1) end. match goal with |- 0+1=1 => trivial end. Qed. + +(* Mini-check that no_check does not check *) + +Goal True -> False. +intro H. +change_no_check nat. +apply S. +change_no_check nat with bool. +change_no_check nat in H. +change_no_check nat with (bool->bool) in H. +exact (H true). +Fail Qed. +Abort. |