diff options
Diffstat (limited to 'test-suite')
43 files changed, 1651 insertions, 10 deletions
diff --git a/test-suite/bugs/closed/bug_10812.v b/test-suite/bugs/closed/bug_10812.v new file mode 100644 index 0000000000..68f3814781 --- /dev/null +++ b/test-suite/bugs/closed/bug_10812.v @@ -0,0 +1,28 @@ +(* subst with indirectly dependent section variables *) + +Section A. + +Variable a:nat. +Definition b := a. + +Goal a=1 -> a+a=1 -> b=1. +intros. +Fail subst a. (* was working; we make it failing *) +rewrite H in H0. +discriminate. +Qed. + +Goal a=1 -> a+a=1 -> b=1. +intros. +subst. (* should not apply to a *) +rewrite H in H0. +discriminate. +Qed. + +Goal forall t, a=t -> b=t. +intros. +subst. +reflexivity. +Qed. + +End A. diff --git a/test-suite/bugs/closed/bug_11727.v b/test-suite/bugs/closed/bug_11727.v new file mode 100644 index 0000000000..d346f05c10 --- /dev/null +++ b/test-suite/bugs/closed/bug_11727.v @@ -0,0 +1,8 @@ +Tactic Notation "myunfold" reference(x) := unfold x. +Notation idnat := (@id nat). +Goal let n := 0 in idnat n = 0. +Proof. + intro n. + myunfold idnat. + myunfold n. +Abort. diff --git a/test-suite/bugs/closed/bug_12196.v b/test-suite/bugs/closed/bug_12196.v new file mode 100644 index 0000000000..c0851b3204 --- /dev/null +++ b/test-suite/bugs/closed/bug_12196.v @@ -0,0 +1,46 @@ +(** TODO: Figure out how to test "sanity" for the ltac profiler output *) +Fixpoint fact (n : nat) := match n with 0 => 1 | S n' => n * fact n' end. +Fixpoint walk (n : nat) := match n with 0 => tt | S n => walk n end. +Ltac slow := idtac + (do 2 (let x := eval lazy in (walk (fact 9)) in idtac)). +Ltac slow2 := idtac + (do 2 (let x := eval lazy in (walk (fact 9)) in idtac)). +Ltac multi := idtac + slow + slow2. +Set Ltac Profiling. +Goal True. + Time try (multi; fail). + (* Warning: Ltac Profiler cannot yet handle backtracking into multi-success + tactics; profiling results may be wildly inaccurate. + [profile-backtracking,ltac] *) + Show Ltac Profile. + (* Used to be: +total time: 0.000s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─multi --------------------------------- 47.1% 47.1% 1 0.000s +─slow ---------------------------------- 35.3% 35.3% 1 0.000s +─slow2 --------------------------------- 17.6% 17.6% 1 0.000s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─multi --------------------------------- 47.1% 47.1% 1 0.000s +─slow ---------------------------------- 35.3% 35.3% 1 0.000s +─slow2 --------------------------------- 17.6% 17.6% 1 0.000s + + *) + (* Now: +total time: 2.074s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─multi --------------------------------- 0.0% 100.0% 6 1.119s +─slow ---------------------------------- 54.0% 54.0% 3 1.119s +─slow2 --------------------------------- 46.0% 46.0% 3 0.955s + + tactic local total calls max +────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ +─multi --------------------------------- 0.0% 100.0% 6 1.119s + ├─slow -------------------------------- 54.0% 54.0% 3 1.119s + └─slow2 ------------------------------- 46.0% 46.0% 3 0.955s + +*) +Abort. diff --git a/test-suite/bugs/closed/bug_12234.v b/test-suite/bugs/closed/bug_12234.v new file mode 100644 index 0000000000..b99c5d524e --- /dev/null +++ b/test-suite/bugs/closed/bug_12234.v @@ -0,0 +1,9 @@ +(* Checking a Show Proof bug *) +Section S. +Variable A:Prop. +Theorem thm (a:A) : True. +assert (b:=a). +clear A a b. +Show Proof. +Abort. +End S. diff --git a/test-suite/bugs/closed/bug_12257.v b/test-suite/bugs/closed/bug_12257.v new file mode 100644 index 0000000000..4962048a42 --- /dev/null +++ b/test-suite/bugs/closed/bug_12257.v @@ -0,0 +1,3 @@ +(* Test that ExtrHaskellString transitively requires ExtrHaskellBasic *) +Require Coq.extraction.ExtrHaskellString. +Import Coq.extraction.ExtrHaskellBasic. diff --git a/test-suite/bugs/closed/bug_2830.v b/test-suite/bugs/closed/bug_2830.v index a321bb324e..16ba02b340 100644 --- a/test-suite/bugs/closed/bug_2830.v +++ b/test-suite/bugs/closed/bug_2830.v @@ -208,7 +208,7 @@ Defined. (* The [list] type constructor is a Functor. *) -Import List. +Require Import List. Definition setList (A:set_cat) := list A. Instance list_functor : Functor set_cat set_cat setList. diff --git a/test-suite/bugs/closed/bug_4151.v b/test-suite/bugs/closed/bug_4151.v index 9ec8c01ac6..df3c9481a6 100644 --- a/test-suite/bugs/closed/bug_4151.v +++ b/test-suite/bugs/closed/bug_4151.v @@ -9,7 +9,7 @@ Qed. Axiom proof_admitted : False. Tactic Notation "admit" := case proof_admitted. Require Import Coq.Lists.SetoidList. -Require Export Coq.Program.Program. +Import ListNotations. Global Set Implicit Arguments. Global Set Asymmetric Patterns. diff --git a/test-suite/bugs/closed/bug_4925.v b/test-suite/bugs/closed/bug_4925.v new file mode 100644 index 0000000000..d4e4b35351 --- /dev/null +++ b/test-suite/bugs/closed/bug_4925.v @@ -0,0 +1,6 @@ +Axiom a: bool. + +Goal a = true. +Proof. +try unfold a. +Abort. diff --git a/test-suite/bugs/closed/bug_5159.v b/test-suite/bugs/closed/bug_5159.v new file mode 100644 index 0000000000..cbc924c2d3 --- /dev/null +++ b/test-suite/bugs/closed/bug_5159.v @@ -0,0 +1,12 @@ +Axiom foo : Type. +Definition bar := 1. +Definition bar' := Eval cbv -[bar] in bar. +Declare Reduction red' := cbv -[bar]. +Opaque bar. +Definition bar'' := Eval red' in bar. +Declare Reduction red'' := cbv -[bar]. (* Error: Cannot coerce bar to an +evaluable reference. *) +Definition bar''' := Eval cbv -[bar] in bar. (* Error: Cannot coerce bar to an +evaluable reference. *) +Definition foo' := Eval cbv -[foo] in foo. (* Error: Cannot coerce foo to an +evaluable reference. *) diff --git a/test-suite/bugs/closed/bug_5764.v b/test-suite/bugs/closed/bug_5764.v new file mode 100644 index 0000000000..0b015d9c7e --- /dev/null +++ b/test-suite/bugs/closed/bug_5764.v @@ -0,0 +1,7 @@ +Module Type A. +Parameter a : nat. +End A. + +Module B (mA : A). +Ltac cbv_a := cbv [mA.a]. +End B. diff --git a/test-suite/bugs/closed/bug_6378.v b/test-suite/bugs/closed/bug_6378.v index 68ae7961dd..453924d587 100644 --- a/test-suite/bugs/closed/bug_6378.v +++ b/test-suite/bugs/closed/bug_6378.v @@ -7,11 +7,20 @@ Ltac profile_constr tac := Ltac slow _ := eval vm_compute in (Z.div_eucl, Z.div_eucl, Z.div_eucl, Z.div_eucl, Z.div_eucl). +Ltac manipulate_ltac_prof := + start ltac profiling; + reset ltac profile; + try ((idtac + reset ltac profile + idtac); fail); + try ((idtac + start ltac profiling + idtac); fail); + try ((idtac + stop ltac profiling + idtac); fail). + Goal True. start ltac profiling. reset ltac profile. + manipulate_ltac_prof. reset ltac profile. stop ltac profiling. + Set Warnings Append "+profile-invalid-stack-no-self". time profile_constr slow. show ltac profile cutoff 0. show ltac profile "slow". diff --git a/test-suite/bugs/closed/bug_7903.v b/test-suite/bugs/closed/bug_7903.v index 55c7ee99a7..18e1884ca7 100644 --- a/test-suite/bugs/closed/bug_7903.v +++ b/test-suite/bugs/closed/bug_7903.v @@ -1,4 +1,4 @@ (* Slightly improving interpretation of Ltac subterms in notations *) Notation bar x f := (let z := ltac:(exact 1) in (fun x : nat => f)). -Check bar x (x + x). +Check fun x => bar x (x + x). diff --git a/test-suite/bugs/closed/bug_9583.v b/test-suite/bugs/closed/bug_9583.v new file mode 100644 index 0000000000..14232e8578 --- /dev/null +++ b/test-suite/bugs/closed/bug_9583.v @@ -0,0 +1,7 @@ +(* Was causing a stack overflow before #11613 *) +Declare Custom Entry bla. +Notation "[ t ]" := (t) (at level 0, t custom bla at level 0). +Notation "] t [" := (t) (in custom bla at level 0, t custom bla at level 0). +Notation "t" := (t) (in custom bla at level 0, t constr at level 9). +Notation "0" := (0) (in custom bla at level 0). +Check fun x => [ ] x [ ]. diff --git a/test-suite/bugs/closed/bug_9679.v b/test-suite/bugs/closed/bug_9679.v new file mode 100644 index 0000000000..24e69d23f9 --- /dev/null +++ b/test-suite/bugs/closed/bug_9679.v @@ -0,0 +1,6 @@ +(* Was raising an anomaly *) +Notation "'[#' ] f '|' x .. z '=n>' b" := + (fun x => .. (fun z => f b) ..) + (at level 201, x binder, z binder, + format "'[ ' [# ] '[' f | ']' x .. z =n> '[' b ']' ']'" + ). diff --git a/test-suite/ltac2/rebind.v b/test-suite/ltac2/rebind.v index e1c20a2059..7b3a460c8c 100644 --- a/test-suite/ltac2/rebind.v +++ b/test-suite/ltac2/rebind.v @@ -15,6 +15,39 @@ Fail foo (). constructor. Qed. + +(** Bindings are dynamic *) + +Ltac2 Type rec nat := [O | S (nat)]. + +Ltac2 rec nat_eq n m := + match n with + | O => match m with | O => true | S _ => false end + | S n => match m with | O => false | S m => nat_eq n m end + end. + +Ltac2 Type exn ::= [ Assertion_failed ]. + +Ltac2 assert_eq n m := + match nat_eq n m with + | true => () + | false => Control.throw Assertion_failed end. + +Ltac2 mutable x := O. +Ltac2 y := x. +Ltac2 Eval (assert_eq y O). +Ltac2 Set x := (S O). +Ltac2 Eval (assert_eq y (S O)). + +Ltac2 mutable quw := fun (n : nat) => O. +Ltac2 Set quw := fun n => + match n with + | O => O + | S n => S (S (quw n)) + end. + +Ltac2 Eval (quw (S (S O))). + (** Not the right type *) Fail Ltac2 Set foo := 0. @@ -25,10 +58,46 @@ Fail Ltac2 Set bar := fun _ => (). (** Subtype check *) -Ltac2 mutable rec f x := f x. +Ltac2 rec h x := h x. +Ltac2 mutable f x := h x. Fail Ltac2 Set f := fun x => x. Ltac2 mutable g x := x. +Ltac2 Set g := h. + +(** Rebinding with old values *) + + + +Ltac2 mutable qux n := S n. + +Ltac2 Set qux as self := fun n => self (self n). + +Ltac2 Eval assert_eq (qux O) (S (S O)). + +Ltac2 mutable quz := O. + +Ltac2 Set quz as self := S self. + +Ltac2 Eval (assert_eq quz (S O)). + +Ltac2 rec addn n := + match n with + | O => fun m => m + | S n => fun m => S (addn n m) + + end. +Ltac2 mutable rec quy n := + match n with + | O => S O + | S n => S (quy n) + end. -Ltac2 Set g := f. +Ltac2 Set quy as self := fun n => + match n with + | O => O + | S n => addn (self n) (quy n) + end. +Ltac2 Eval (assert_eq (quy (S (S O))) (S (S (S O)))). +Ltac2 Eval (assert_eq (quy (S (S (S O)))) (S (S (S (S (S (S O))))))). diff --git a/test-suite/output/ErrorLocation_12152_1.out b/test-suite/output/ErrorLocation_12152_1.out new file mode 100644 index 0000000000..b7b600d53d --- /dev/null +++ b/test-suite/output/ErrorLocation_12152_1.out @@ -0,0 +1,3 @@ +File "stdin", line 3, characters 0-7: +Error: No product even after head-reduction. + diff --git a/test-suite/output/ErrorLocation_12152_1.v b/test-suite/output/ErrorLocation_12152_1.v new file mode 100644 index 0000000000..e63ab1cd48 --- /dev/null +++ b/test-suite/output/ErrorLocation_12152_1.v @@ -0,0 +1,3 @@ +(* Reported in #12152 *) +Goal True. +intro H; auto. diff --git a/test-suite/output/ErrorLocation_12152_2.out b/test-suite/output/ErrorLocation_12152_2.out new file mode 100644 index 0000000000..bdfd0a050f --- /dev/null +++ b/test-suite/output/ErrorLocation_12152_2.out @@ -0,0 +1,3 @@ +File "stdin", line 3, characters 0-8: +Error: No product even after head-reduction. + diff --git a/test-suite/output/ErrorLocation_12152_2.v b/test-suite/output/ErrorLocation_12152_2.v new file mode 100644 index 0000000000..5df6bec939 --- /dev/null +++ b/test-suite/output/ErrorLocation_12152_2.v @@ -0,0 +1,3 @@ +(* Reported in #12152 *) +Goal True. +intros H; auto. diff --git a/test-suite/output/ErrorLocation_12255.out b/test-suite/output/ErrorLocation_12255.out new file mode 100644 index 0000000000..ed5e183427 --- /dev/null +++ b/test-suite/output/ErrorLocation_12255.out @@ -0,0 +1,4 @@ +File "stdin", line 4, characters 0-16: +Error: Ltac variable x is bound to i > 0 which cannot be coerced to +an evaluable reference. + diff --git a/test-suite/output/ErrorLocation_12255.v b/test-suite/output/ErrorLocation_12255.v new file mode 100644 index 0000000000..347424b2fc --- /dev/null +++ b/test-suite/output/ErrorLocation_12255.v @@ -0,0 +1,4 @@ +Ltac can_unfold x := let b := eval cbv delta [x] in x in idtac. +Definition i := O. +Goal False. +can_unfold (i>0). diff --git a/test-suite/output/Extraction_Haskell_String_12258.out b/test-suite/output/Extraction_Haskell_String_12258.out new file mode 100644 index 0000000000..615abaa3e8 --- /dev/null +++ b/test-suite/output/Extraction_Haskell_String_12258.out @@ -0,0 +1,73 @@ +{-# OPTIONS_GHC -cpp -XMagicHash #-} +{- For Hugs, use the option -F"cpp -P -traditional" -} + +{- IMPORTANT: If you change this file, make sure that running [cp + Extraction_Haskell_String_12258.out Extraction_Haskell_String_12258.hs && + ghc -o test Extraction_Haskell_String_12258.hs] succeeds -} + +module Main where + +import qualified Prelude + +#ifdef __GLASGOW_HASKELL__ +import qualified GHC.Base +#else +-- HUGS +import qualified IOExts +#endif + +#ifdef __GLASGOW_HASKELL__ +unsafeCoerce :: a -> b +unsafeCoerce = GHC.Base.unsafeCoerce# +#else +-- HUGS +unsafeCoerce :: a -> b +unsafeCoerce = IOExts.unsafeCoerce +#endif + +#ifdef __GLASGOW_HASKELL__ +type Any = GHC.Base.Any +#else +-- HUGS +type Any = () +#endif + +data Output_type_code = + Ascii_dec + | Ascii_eqb + | String_dec + | String_eqb + | Byte_eqb + | Byte_eq_dec + +type Output_type = Any + +output :: Output_type_code -> Output_type +output c = + case c of { + Ascii_dec -> + unsafeCoerce + ((Prelude.==) :: Prelude.Char -> Prelude.Char -> Prelude.Bool); + Ascii_eqb -> + unsafeCoerce + ((Prelude.==) :: Prelude.Char -> Prelude.Char -> Prelude.Bool); + String_dec -> + unsafeCoerce + ((Prelude.==) :: Prelude.String -> Prelude.String -> Prelude.Bool); + String_eqb -> + unsafeCoerce + ((Prelude.==) :: Prelude.String -> Prelude.String -> Prelude.Bool); + Byte_eqb -> + unsafeCoerce + ((Prelude.==) :: Prelude.Char -> Prelude.Char -> Prelude.Bool); + Byte_eq_dec -> + unsafeCoerce + ((Prelude.==) :: Prelude.Char -> Prelude.Char -> Prelude.Bool)} + +type Coq__IO a = GHC.Base.IO a + +main :: GHC.Base.IO () +main = + ((Prelude.>>=) (GHC.Base.return output) (\_ -> GHC.Base.return ())) + + diff --git a/test-suite/output/Extraction_Haskell_String_12258.v b/test-suite/output/Extraction_Haskell_String_12258.v new file mode 100644 index 0000000000..063ff64337 --- /dev/null +++ b/test-suite/output/Extraction_Haskell_String_12258.v @@ -0,0 +1,52 @@ +Require Import Coq.extraction.Extraction. +Require Import Coq.extraction.ExtrHaskellString. +Extraction Language Haskell. +Set Extraction File Comment "IMPORTANT: If you change this file, make sure that running [cp Extraction_Haskell_String_12258.out Extraction_Haskell_String_12258.hs && ghc -o test Extraction_Haskell_String_12258.hs] succeeds". +Inductive output_type_code := +| ascii_dec +| ascii_eqb +| string_dec +| string_eqb +| byte_eqb +| byte_eq_dec +. + +Definition output_type_sig (c : output_type_code) : { T : Type & T } + := existT (fun T => T) + _ + match c return match c with ascii_dec => _ | _ => _ end with + | ascii_dec => Ascii.ascii_dec + | ascii_eqb => Ascii.eqb + | string_dec => String.string_dec + | string_eqb => String.eqb + | byte_eqb => Byte.eqb + | byte_eq_dec => Byte.byte_eq_dec + end. + +Definition output_type (c : output_type_code) + := Eval cbv [output_type_sig projT1 projT2] in + projT1 (output_type_sig c). +Definition output (c : output_type_code) : output_type c + := Eval cbv [output_type_sig projT1 projT2] in + match c return output_type c with + | ascii_dec as c + | _ as c + => projT2 (output_type_sig c) + end. + +Axiom IO_unit : Set. +Axiom _IO : Set -> Set. +Axiom _IO_bind : forall {A B}, _IO A -> (A -> _IO B) -> _IO B. +Axiom _IO_return : forall {A : Set}, A -> _IO A. +Axiom cast_io : _IO unit -> IO_unit. +Extract Constant _IO "a" => "GHC.Base.IO a". +Extract Inlined Constant _IO_bind => "(Prelude.>>=)". +Extract Inlined Constant _IO_return => "GHC.Base.return". +Extract Inlined Constant IO_unit => "GHC.Base.IO ()". +Extract Inlined Constant cast_io => "". + +Definition main : IO_unit + := cast_io (_IO_bind (_IO_return output) + (fun _ => _IO_return tt)). + +Recursive Extraction main. diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out index 60bc9cbf55..ff7918b4e6 100644 --- a/test-suite/output/Fixpoint.out +++ b/test-suite/output/Fixpoint.out @@ -12,3 +12,27 @@ let fix f (m : nat) : nat := match m with Ltac f id1 id2 := fix id1 2 with (id2 (n:_) (H:odd n) {struct H} : n >= 1) = cofix inf : Inf := {| projS := inf |} : Inf +File "stdin", line 57, characters 0-51: +Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints] +File "stdin", line 60, characters 0-103: +Warning: Not a fully mutually defined fixpoint +(k1 depends on k2 but not conversely). +Well-foundedness check may fail unexpectedly. + [non-full-mutual,fixpoints] +File "stdin", line 62, characters 0-106: +Warning: Not a fully mutually defined fixpoint +(l2 and l1 are not mutually dependent). +Well-foundedness check may fail unexpectedly. + [non-full-mutual,fixpoints] +File "stdin", line 64, characters 0-103: +Warning: Not a fully mutually defined fixpoint +(m2 and m1 are not mutually dependent). +Well-foundedness check may fail unexpectedly. + [non-full-mutual,fixpoints] +File "stdin", line 72, characters 0-25: +Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints] +File "stdin", line 75, characters 0-48: +Warning: Not a fully mutually defined fixpoint +(a2 and a1 are not mutually dependent). +Well-foundedness check may fail unexpectedly. + [non-full-mutual,fixpoints] diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v index 398528de72..26c276b68b 100644 --- a/test-suite/output/Fixpoint.v +++ b/test-suite/output/Fixpoint.v @@ -44,7 +44,39 @@ fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1). lia. Qed. -CoInductive Inf := S { projS : Inf }. -Definition expand_Inf (x : Inf) := S (projS x). -CoFixpoint inf := S inf. +CoInductive Inf := IS { projS : Inf }. +Definition expand_Inf (x : Inf) := IS (projS x). +CoFixpoint inf := IS inf. Eval compute in inf. + +Module Recursivity. + +Open Scope nat_scope. + +Fixpoint f n := match n with 0 => 0 | S n => f n end. +Fixpoint g n := match n with 0 => 0 | S n => n end. +Fixpoint h1 n := match n with 0 => 0 | S n => h2 n end +with h2 n := match n with 0 => 0 | S n => h1 n end. +Fixpoint k1 n := match n with 0 => 0 | S n => k2 n end +with k2 n := match n with 0 => 0 | S n => n end. +Fixpoint l1 n := match n with 0 => 0 | S n => l1 n end +with l2 n := match n with 0 => 0 | S n => l2 n end. +Fixpoint m1 n := match n with 0 => 0 | S n => m1 n end +with m2 n := match n with 0 => 0 | S n => n end. +(* Why not to allow this definition ? +Fixpoint h1' n := match n with 0 => 0 | S n => h2' n end +with h2' n := h1' n. +*) +CoInductive S := cons : nat -> S -> S. +CoFixpoint c := cons 0 c. +CoFixpoint d := cons 0 c. +CoFixpoint e1 := cons 0 e2 +with e2 := cons 1 e1. +CoFixpoint a1 := cons 0 a1 +with a2 := cons 1 a2. +(* Why not to allow this definition ? +CoFixpoint b1 := cons 0 b2 +with b2 := b1. +*) + +End Recursivity. diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index f48eaac4c9..9cb019ca56 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -111,3 +111,11 @@ Warning: The format modifier is irrelevant for only parsing rules. File "stdin", line 280, characters 0-63: Warning: The only parsing modifier has no effect in Reserved Notation. [irrelevant-reserved-notation-only-parsing,parsing] +fun x : nat => U (S x) + : nat -> nat +V tt + : unit * (unit -> unit) +fun x : nat => V x + : forall x : nat, nat * (?T -> ?T) +where +?T : [x : nat x0 : ?T |- Type] (x0 cannot be used) diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 4d4b37a8b2..b3270d4f92 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -280,3 +280,13 @@ Notation "###" := 0 (at level 0, only parsing, format "###"). Reserved Notation "##" (at level 0, only parsing, format "##"). End N. + +Module O. + +Notation U t := (match t with 0 => 0 | S t => t | _ => 0 end). +Check fun x => U (S x). +Notation V t := (t,fun t => t). +Check V tt. +Check fun x : nat => V x. + +End O. diff --git a/test-suite/output/bug_12159.out b/test-suite/output/bug_12159.out new file mode 100644 index 0000000000..7f47c47e32 --- /dev/null +++ b/test-suite/output/bug_12159.out @@ -0,0 +1,28 @@ +f 1%B + : unit +f 0 + : unit +1%B + : unit +0 + : unit +1%B + : unit +1 + : unit +1 + : unit +0 + : unit +1 + : unit +0%A + : unit +1 + : unit +0%A + : unit +0 + : unit +0 + : unit diff --git a/test-suite/output/bug_12159.v b/test-suite/output/bug_12159.v new file mode 100644 index 0000000000..91d66f7f4c --- /dev/null +++ b/test-suite/output/bug_12159.v @@ -0,0 +1,39 @@ +Declare Scope A. +Declare Scope B. +Delimit Scope A with A. +Delimit Scope B with B. +Definition to_unit (v : Decimal.uint) : option unit + := match Nat.of_uint v with O => Some tt | _ => None end. +Definition of_unit (v : unit) : Decimal.uint := Nat.to_uint 0. +Definition of_unit' (v : unit) : Decimal.uint := Nat.to_uint 1. +Numeral Notation unit to_unit of_unit : A. +Numeral Notation unit to_unit of_unit' : B. +Definition f x : unit := x. +Check f tt. +Arguments f x%A. +Check f tt. +Check tt. +Open Scope A. +Check tt. +Close Scope A. +Check tt. +Open Scope B. +Check tt. +Undelimit Scope B. +Check tt. +Open Scope A. +Check tt. +Close Scope A. +Check tt. +Close Scope B. +Check tt. +Open Scope B. +Check tt. +Notation "1" := true. +Check tt. +Open Scope A. +Check tt. +Declare Scope C. +Notation "0" := false : C. +Open Scope C. +Check tt. (* gives 0 but should now be 0%A *) diff --git a/test-suite/output/interleave_options_bad_order.out b/test-suite/output/interleave_options_bad_order.out new file mode 100644 index 0000000000..68dbaeb7b3 --- /dev/null +++ b/test-suite/output/interleave_options_bad_order.out @@ -0,0 +1,4 @@ +While loading initial state: +Warning: There is no flag or option with this name: "Extraction Optimize". +[unknown-option,option] +Extraction Optimize is on diff --git a/test-suite/output/interleave_options_bad_order.v b/test-suite/output/interleave_options_bad_order.v new file mode 100644 index 0000000000..9a70674b02 --- /dev/null +++ b/test-suite/output/interleave_options_bad_order.v @@ -0,0 +1,3 @@ +(* coq-prog-args: ("-unset" "Extraction Optimize" "-ri" "Extraction") *) + +Test Extraction Optimize. diff --git a/test-suite/output/interleave_options_correct_order.out b/test-suite/output/interleave_options_correct_order.out new file mode 100644 index 0000000000..76bb2016eb --- /dev/null +++ b/test-suite/output/interleave_options_correct_order.out @@ -0,0 +1 @@ +Extraction Optimize is off diff --git a/test-suite/output/interleave_options_correct_order.v b/test-suite/output/interleave_options_correct_order.v new file mode 100644 index 0000000000..7622d6ff52 --- /dev/null +++ b/test-suite/output/interleave_options_correct_order.v @@ -0,0 +1,3 @@ +(* coq-prog-args: ("-ri" "Extraction" "-unset" "Extraction Optimize") *) + +Test Extraction Optimize. diff --git a/test-suite/output/print_ltac.out b/test-suite/output/print_ltac.out index 952761acca..58931c4b82 100644 --- a/test-suite/output/print_ltac.out +++ b/test-suite/output/print_ltac.out @@ -6,3 +6,340 @@ Ltac t3 := idtacstr "my tactic" Ltac t4 x := match x with | ?A => (A, A) end +The command has indeed failed with message: +idnat is bound to a notation that does not denote a reference. +Ltac withstrategy l x := + let idx := smart_global:(id) in + let tl := strategy_level:(transparent) in + with_strategy + 1 + [ + id + id + ] + with_strategy + l + [ + id + id + ] + with_strategy + tl + [ + id + id + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + opaque + [ + id + id + ] + with_strategy + expand + [ + id + id + ] + with_strategy + transparent + [ + idx + ] + with_strategy + transparent + [ + id + x + ] + with_strategy + transparent + [ + x + id + ] + with_strategy + transparent + [ + id + ] + with_strategy + transparent + [ + id + x + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + transparent + [ + id + id + x + ] + with_strategy + transparent + [ + id + ] + with_strategy + transparent + [ + id + x + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + transparent + [ + id + id + x + ] + idtac +The command has indeed failed with message: +idnat is bound to a notation that does not denote a reference. +Ltac withstrategy l x := + let idx := smart_global:(id) in + let tl := strategy_level:(transparent) in + with_strategy + 1 + [ + id + id + ] + with_strategy + l + [ + id + id + ] + with_strategy + tl + [ + id + id + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + opaque + [ + id + id + ] + with_strategy + expand + [ + id + id + ] + with_strategy + transparent + [ + idx + ] + with_strategy + transparent + [ + id + x + ] + with_strategy + transparent + [ + x + id + ] + with_strategy + transparent + [ + id + ] + with_strategy + transparent + [ + id + x + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + transparent + [ + id + id + x + ] + with_strategy + transparent + [ + id + ] + with_strategy + transparent + [ + id + x + ] + with_strategy + transparent + [ + id + id + ] + with_strategy + transparent + [ + id + id + x + ] + idtac +Ltac FE.withstrategy l x := + let idx := smart_global:(FE.id) in + let tl := strategy_level:(transparent) in + with_strategy + 1 + [ + FE.id + FE.id + ] + with_strategy + l + [ + FE.id + FE.id + ] + with_strategy + tl + [ + FE.id + FE.id + ] + with_strategy + transparent + [ + FE.id + FE.id + ] + with_strategy + transparent + [ + FE.id + FE.id + ] + with_strategy + opaque + [ + FE.id + FE.id + ] + with_strategy + expand + [ + FE.id + FE.id + ] + with_strategy + transparent + [ + idx + ] + with_strategy + transparent + [ + FE.id + x + ] + with_strategy + transparent + [ + x + FE.id + ] + with_strategy + transparent + [ + FE.id + ] + with_strategy + transparent + [ + FE.id + x + ] + with_strategy + transparent + [ + FE.id + FE.id + ] + with_strategy + transparent + [ + FE.id + FE.id + x + ] + with_strategy + transparent + [ + FE.id + ] + with_strategy + transparent + [ + FE.id + x + ] + with_strategy + transparent + [ + FE.id + FE.id + ] + with_strategy + transparent + [ + FE.id + FE.id + x + ] + idtac diff --git a/test-suite/output/print_ltac.v b/test-suite/output/print_ltac.v index a992846791..d0883e32e4 100644 --- a/test-suite/output/print_ltac.v +++ b/test-suite/output/print_ltac.v @@ -10,3 +10,73 @@ Print Ltac t3. (* https://github.com/coq/coq/issues/9716 *) Ltac t4 x := match x with ?A => constr:((A, A)) end. Print Ltac t4. + +Notation idnat := (@id nat). +Notation idn := id. +Notation idan := (@id). +Fail Strategy transparent [idnat]. +Strategy transparent [idn]. +Strategy transparent [idan]. +Ltac withstrategy l x := + let idx := smart_global:(id) in + let tl := strategy_level:(transparent) in + with_strategy 1 [id id] ( + with_strategy l [id id] ( + with_strategy tl [id id] ( + with_strategy 0 [id id] ( + with_strategy transparent [id id] ( + with_strategy opaque [id id] ( + with_strategy expand [id id] ( + with_strategy 0 [idx] ( + with_strategy 0 [id x] ( + with_strategy 0 [x id] ( + with_strategy 0 [idn] ( + with_strategy 0 [idn x] ( + with_strategy 0 [idn id] ( + with_strategy 0 [idn id x] ( + with_strategy 0 [idan] ( + with_strategy 0 [idan x] ( + with_strategy 0 [idan id] ( + with_strategy 0 [idan id x] ( + idtac + )))))))))))))))))). +Print Ltac withstrategy. + +Module Type Empty. End Empty. +Module E. End E. +Module F (E : Empty). + Definition id {T} := @id T. + Notation idnat := (@id nat). + Notation idn := id. + Notation idan := (@id). + Fail Strategy transparent [idnat]. + Strategy transparent [idn]. + Strategy transparent [idan]. + Ltac withstrategy l x := + let idx := smart_global:(id) in + let tl := strategy_level:(transparent) in + with_strategy 1 [id id] ( + with_strategy l [id id] ( + with_strategy tl [id id] ( + with_strategy 0 [id id] ( + with_strategy transparent [id id] ( + with_strategy opaque [id id] ( + with_strategy expand [id id] ( + with_strategy 0 [idx] ( + with_strategy 0 [id x] ( + with_strategy 0 [x id] ( + with_strategy 0 [idn] ( + with_strategy 0 [idn x] ( + with_strategy 0 [idn id] ( + with_strategy 0 [idn id x] ( + with_strategy 0 [idan] ( + with_strategy 0 [idan x] ( + with_strategy 0 [idan id] ( + with_strategy 0 [idan id x] ( + idtac + )))))))))))))))))). + Print Ltac withstrategy. +End F. + +Module FE := F E. +Print Ltac FE.withstrategy. diff --git a/test-suite/ssr/simpl_done.v b/test-suite/ssr/simpl_done.v new file mode 100644 index 0000000000..f5c766209a --- /dev/null +++ b/test-suite/ssr/simpl_done.v @@ -0,0 +1,28 @@ +Require Import ssreflect. + +Inductive lit : Set := +| LitP : lit +| LitL : lit +. + +Inductive val : Set := +| Val : lit -> val. + +Definition tyref := +fun (vl : list val) => +match vl with +| cons (Val LitL) (cons (Val LitP) _) => False +| _ => False +end. + +(** Check that simplification and resolution are performed in the right order + by "//=" when several goals are under focus. *) +Goal exists vl1 : list val, + cons (Val LitL) (cons (Val LitL) nil) = vl1 /\ + (tyref vl1) +. +Proof. +eexists (cons _ (cons _ _)). +split =>//=. +Fail progress simpl. +Abort. diff --git a/test-suite/ssr/try_case.v b/test-suite/ssr/try_case.v new file mode 100644 index 0000000000..114bf2cecf --- /dev/null +++ b/test-suite/ssr/try_case.v @@ -0,0 +1,11 @@ +From Coq Require Import ssreflect. + +Axiom T : Type. +Axiom R : T -> T -> Type. + +(** Check that internal exceptions are correctly caught in the monad *) +Goal forall (a b : T) (Hab : R a b), True. +Proof. +intros. +try (case: Hab). +Abort. diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v index 18ebcd6384..ce07512a1e 100644 --- a/test-suite/success/Record.v +++ b/test-suite/success/Record.v @@ -3,6 +3,7 @@ Definition CProp := Prop. Record test : CProp := {n : nat ; m : bool ; _ : n <> 0 }. Require Import Program. Require Import List. +Import ListNotations. Record vector {A : Type} {n : nat} := { vec_list : list A ; vec_len : length vec_list = n }. Arguments vector : clear implicits. diff --git a/test-suite/success/ltacprof.v b/test-suite/success/ltacprof.v index d5552695c4..f40f40c2bb 100644 --- a/test-suite/success/ltacprof.v +++ b/test-suite/success/ltacprof.v @@ -6,3 +6,20 @@ Goal True. try (multi; fail). (* Used to result in: Anomaly: Uncaught exception Failure("hd"). Please report. *) Admitted. Show Ltac Profile. + +(* backtracking across profiler manipulation *) +Unset Ltac Profiling. +Reset Ltac Profile. + +Fixpoint slow (n : nat) : unit + := match n with + | 0 => tt + | S n => fst (slow n, slow n) + end. + +Ltac slow := idtac; let v := eval cbv in (slow 16) in idtac. +Ltac multi2 := + try (((idtac; slow) + (start ltac profiling; slow) + (idtac; slow) + (slow; stop ltac profiling; slow) + slow + (start ltac profiling; (idtac + slow); ((stop ltac profiling + idtac); fail))); slow; fail); slow; show ltac profile. +Goal True. + multi2. +Admitted. diff --git a/test-suite/success/shrink_obligations.v b/test-suite/success/shrink_obligations.v index 676b97878f..032fcaac6d 100644 --- a/test-suite/success/shrink_obligations.v +++ b/test-suite/success/shrink_obligations.v @@ -2,8 +2,6 @@ Require Program. Obligation Tactic := idtac. -Set Shrink Obligations. - Program Definition foo (m : nat) (p := S m) (n : nat) (q := S n) : unit := let bar : {r | n < r} := _ in let qux : {r | p < r} := _ in diff --git a/test-suite/success/strategy.v b/test-suite/success/strategy.v new file mode 100644 index 0000000000..926ba54342 --- /dev/null +++ b/test-suite/success/strategy.v @@ -0,0 +1,87 @@ +Notation aid := (@id) (only parsing). +Notation idn := id (only parsing). +Ltac unfold_id := unfold id. + +Fixpoint fact (n : nat) + := match n with + | 0 => 1 + | S n => (S n) * fact n + end. + +Opaque id. +Goal id (fact 100) = fact 100. + Strategy expand [id]. + Time Timeout 5 reflexivity. (* should be instant *) + (* Finished transaction in 0. secs (0.u,0.s) (successful) *) +Time Timeout 5 Defined. +(* Finished transaction in 0.001 secs (0.u,0.s) (successful) *) + +Goal True. + let x := smart_global:(id) in unfold x. + let x := smart_global:(aid) in unfold x. + let x := smart_global:(idn) in unfold x. +Abort. + +Goal id 0 = 0. + Opaque id. + assert_fails unfold_id. + Transparent id. + assert_succeeds unfold_id. + Opaque id. + Strategy 0 [id]. + assert_succeeds unfold_id. + Strategy 1 [id]. + assert_succeeds unfold_id. + Strategy -1 [id]. + assert_succeeds unfold_id. + Strategy opaque [id]. + assert_fails unfold_id. + Strategy transparent [id]. + assert_succeeds unfold_id. + Opaque id. + Strategy expand [id]. + assert_succeeds unfold_id. + reflexivity. +Qed. +Goal id 0 = 0. + Opaque aid. + assert_fails unfold_id. + Transparent aid. + assert_succeeds unfold_id. + Opaque aid. + Strategy 0 [aid]. + assert_succeeds unfold_id. + Strategy 1 [aid]. + assert_succeeds unfold_id. + Strategy -1 [aid]. + assert_succeeds unfold_id. + Strategy opaque [aid]. + assert_fails unfold_id. + Strategy transparent [aid]. + assert_succeeds unfold_id. + Opaque aid. + Strategy expand [aid]. + assert_succeeds unfold_id. + reflexivity. +Qed. +Goal id 0 = 0. + Opaque idn. + assert_fails unfold_id. + Transparent idn. + assert_succeeds unfold_id. + Opaque idn. + Strategy 0 [idn]. + assert_succeeds unfold_id. + Strategy 1 [idn]. + assert_succeeds unfold_id. + Strategy -1 [idn]. + assert_succeeds unfold_id. + Strategy opaque [idn]. + assert_fails unfold_id. + Strategy transparent [idn]. + assert_succeeds unfold_id. + Opaque idn. + Strategy expand [idn]. + assert_succeeds unfold_id. + reflexivity. +Qed. diff --git a/test-suite/success/tac_wit_ref.v b/test-suite/success/tac_wit_ref.v new file mode 100644 index 0000000000..8bde31858e --- /dev/null +++ b/test-suite/success/tac_wit_ref.v @@ -0,0 +1,8 @@ +Tactic Notation "foo" reference(n) := idtac n. + +Goal forall n : nat, n = 0. +Proof. +intros n. +foo nat. +foo n. +Abort. diff --git a/test-suite/success/with_strategy.v b/test-suite/success/with_strategy.v new file mode 100644 index 0000000000..6f0833211e --- /dev/null +++ b/test-suite/success/with_strategy.v @@ -0,0 +1,577 @@ +Notation aid := (@id) (only parsing). +Notation idn := id (only parsing). +Ltac unfold_id := unfold id. + +Fixpoint fact (n : nat) + := match n with + | 0 => 1 + | S n => (S n) * fact n + end. + +Opaque id. +Goal id 0 = 0. + with_strategy + opaque [id] + (with_strategy + opaque [id id] + (assert_fails unfold_id; + with_strategy + transparent [id] + (assert_succeeds unfold_id; + with_strategy + opaque [id] + (with_strategy + 0 [id] + (assert_succeeds unfold_id; + with_strategy + 1 [id] + (assert_succeeds unfold_id; + with_strategy + -1 [id] + (assert_succeeds unfold_id; + with_strategy + opaque [id] + (assert_fails unfold_id; + with_strategy + transparent [id] + (assert_succeeds unfold_id; + with_strategy + opaque [id] + (with_strategy + expand [id] + (assert_succeeds unfold_id; + let l := strategy_level:(expand) in + with_strategy + l [id] + (let idx := smart_global:(id) in + cbv [idx]; + (* This should succeed, but doesn't, basically due to https://github.com/coq/coq/issues/11202 *) + assert_fails + (let idx := smart_global:(id) in + with_strategy + expand [idx] + idtac); + reflexivity)))))))))))). +Qed. +Goal id 0 = 0. + with_strategy + opaque [aid] + (assert_fails unfold_id; + with_strategy + transparent [aid] + (assert_succeeds unfold_id; + with_strategy + opaque [aid] + (with_strategy + 0 [aid] + (assert_succeeds unfold_id; + with_strategy + 1 [aid] + (assert_succeeds unfold_id; + with_strategy + -1 [aid] + (assert_succeeds unfold_id; + with_strategy + opaque [aid] + (assert_fails unfold_id; + with_strategy + transparent [aid] + (assert_succeeds unfold_id; + with_strategy + opaque [aid] + (with_strategy + expand [aid] + (assert_succeeds unfold_id; + reflexivity)))))))))). +Qed. +Goal id 0 = 0. + with_strategy + opaque [idn] + (assert_fails unfold_id; + with_strategy + transparent [idn] + (assert_succeeds unfold_id; + with_strategy + opaque [idn] + (with_strategy + 0 [idn] + (assert_succeeds unfold_id; + with_strategy + 1 [idn] + (assert_succeeds unfold_id; + with_strategy + -1 [idn] + (assert_succeeds unfold_id; + with_strategy + opaque [idn] + (assert_fails unfold_id; + with_strategy + transparent [idn] + (assert_succeeds unfold_id; + with_strategy + opaque [idn] + (with_strategy + expand [idn] + (assert_succeeds unfold_id; + reflexivity)))))))))). +Qed. + +(* test that strategy tactic does not persist after the execution of the tactic *) +Opaque id. +Goal id 0 = 0. + assert_fails unfold_id; + (with_strategy transparent [id] assert_succeeds unfold_id); + assert_fails unfold_id. + assert_fails unfold_id. + with_strategy transparent [id] assert_succeeds unfold_id. + assert_fails unfold_id. + reflexivity. +Qed. + +(* test that the strategy tactic does persist through abstract *) +Opaque id. +Goal id 0 = 0. + Time Timeout 5 + with_strategy + expand [id] + assert (id (fact 100) = fact 100) by abstract reflexivity. + reflexivity. +Time Timeout 5 Defined. + +(* test that it works even with [Qed] *) +Goal id 0 = 0. +Proof using Type. + Time Timeout 5 + abstract + (with_strategy + expand [id] + assert (id (fact 100) = fact 100) by abstract reflexivity; + reflexivity). +Time Timeout 5 Qed. + +(* test that the strategy is correctly reverted after closing the goal completely *) +Goal id 0 = 0. + assert (id 0 = 0) by with_strategy expand [id] reflexivity. + Fail unfold id. + reflexivity. +Qed. + +(* test that the strategy is correctly reverted after failure *) +Goal id 0 = 0. + let id' := id in + (try with_strategy expand [id] fail); assert_fails unfold id'. + Fail unfold id. + (* a more complicated test involving a success and then a failure after backtracking *) + let id' := id in + ((with_strategy expand [id] (unfold id' + fail)) + idtac); + lazymatch goal with |- id 0 = 0 => idtac end; + assert_fails unfold id'. + Fail unfold id. + reflexivity. +Qed. + +(* test multi-success *) +Goal id (fact 100) = fact 100. + Timeout 1 + (with_strategy -1 [id] (((idtac + (abstract reflexivity))); fail)). + Undo. + Timeout 1 + let id' := id in + (with_strategy -1 [id] (((idtac + (unfold id'; reflexivity))); fail)). + Undo. + Timeout 1 + (with_strategy -1 [id] (idtac + (abstract reflexivity))); fail. (* should not time out *) + Undo. + with_strategy -1 [id] abstract reflexivity. +Defined. + +(* check that module substitutions happen correctly *) +Module F. + Definition id {T} := @id T. + Opaque id. + Ltac with_transparent_id tac := with_strategy transparent [id] tac. +End F. +Opaque F.id. + +Goal F.id 0 = F.id 0. + Fail unfold F.id. + F.with_transparent_id ltac:(progress unfold F.id). + Undo. + F.with_transparent_id ltac:(let x := constr:(@F.id) in progress unfold x). +Abort. + +Module Type Empty. End Empty. +Module E. End E. +Module F2F (E : Empty). + Definition id {T} := @id T. + Opaque id. + Ltac with_transparent_id tac := with_strategy transparent [id] tac. +End F2F. +Module F2 := F2F E. +Opaque F2.id. + +Goal F2.id 0 = F2.id 0. + Fail unfold F2.id. + F2.with_transparent_id ltac:(progress unfold F2.id). + Undo. + F2.with_transparent_id ltac:(let x := constr:(@F2.id) in progress unfold x). +Abort. + +(* test the tactic notation entries *) +Tactic Notation "with_strategy0" strategy_level(l) "[" ne_smart_global_list(v) "]" tactic3(tac) := with_strategy l [ v ] tac. +Tactic Notation "with_strategy1" strategy_level_or_var(l) "[" ne_smart_global_list(v) "]" tactic3(tac) := with_strategy l [ v ] tac. +Tactic Notation "with_strategy2" strategy_level(l) "[" constr(v) "]" tactic3(tac) := with_strategy l [ v ] tac. +Tactic Notation "with_strategy3" strategy_level_or_var(l) "[" constr(v) "]" tactic3(tac) := with_strategy l [ v ] tac. + +(* [with_strategy0] should work, but it doesn't, due to a combination of https://github.com/coq/coq/issues/11202 and https://github.com/coq/coq/issues/11209 *) +Opaque id. +Goal id 0 = 0. + Fail (* should work, not Fail *) with_strategy0 opaque [id] idtac. + Fail (* should work, not Fail *) with_strategy0 opaque [id id] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy0 transparent [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 opaque [id] idtac. + Fail (* should work, not Fail *) with_strategy0 0 [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 1 [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 -1 [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 opaque [id] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy0 transparent [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 opaque [id] idtac. + Fail (* should work, not Fail *) with_strategy0 expand [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + (* This should succeed, but doesn't, basically due to https://github.com/coq/coq/issues/11202 *) + Fail let idx := smart_global:(id) in + with_strategy0 expand [idx] idtac. + reflexivity. +Qed. +Goal id 0 = 0. + Fail (* should work, not Fail *) with_strategy0 opaque [aid] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy0 transparent [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 opaque [aid] idtac. + Fail (* should work, not Fail *) with_strategy0 0 [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 1 [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 -1 [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 opaque [aid] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy0 transparent [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 opaque [aid] idtac. + Fail (* should work, not Fail *) with_strategy0 expand [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + reflexivity. +Qed. +Goal id 0 = 0. + Fail (* should work, not Fail *) with_strategy0 opaque [idn] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy0 transparent [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 opaque [idn] idtac. + Fail (* should work, not Fail *) with_strategy0 0 [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 1 [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 -1 [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 opaque [idn] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy0 transparent [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy0 opaque [idn] idtac. + Fail (* should work, not Fail *) with_strategy0 expand [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + reflexivity. +Qed. + +(* [with_strategy1] should work, but it doesn't, due to a combination of https://github.com/coq/coq/issues/11202 and https://github.com/coq/coq/issues/11209 *) +Opaque id. +Goal id 0 = 0. + Fail (* should work, not Fail *) with_strategy1 opaque [id] idtac. + Fail (* should work, not Fail *) with_strategy1 opaque [id id] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy1 transparent [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 opaque [id] idtac. + Fail (* should work, not Fail *) with_strategy1 0 [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 1 [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 -1 [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 opaque [id] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy1 transparent [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 opaque [id] idtac. + Fail (* should work, not Fail *) with_strategy1 expand [id] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) let l := strategy_level:(expand) in + with_strategy1 l [id] idtac. + (* This should succeed, but doesn't, basically due to https://github idtac.com/coq/coq/issues/11202 *) + Fail let idx := smart_global:(id) in + with_strategy1 expand [idx] idtac. + reflexivity. +Qed. +Goal id 0 = 0. + Fail (* should work, not Fail *) with_strategy1 opaque [aid] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy1 transparent [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 opaque [aid] idtac. + Fail (* should work, not Fail *) with_strategy1 0 [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 1 [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 -1 [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 opaque [aid] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy1 transparent [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 opaque [aid] idtac. + Fail (* should work, not Fail *) with_strategy1 expand [aid] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + reflexivity. +Qed. +Goal id 0 = 0. + Fail (* should work, not Fail *) with_strategy1 opaque [idn] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy1 transparent [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 opaque [idn] idtac. + Fail (* should work, not Fail *) with_strategy1 0 [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 1 [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 -1 [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 opaque [idn] idtac. + assert_fails unfold_id. + Fail (* should work, not Fail *) with_strategy1 transparent [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + Fail (* should work, not Fail *) with_strategy1 opaque [idn] idtac. + Fail (* should work, not Fail *) with_strategy1 expand [idn] idtac. + Fail (* should work, not Fail *) assert_succeeds unfold_id idtac. + reflexivity. +Qed. + +Opaque id. +Goal id 0 = 0. + with_strategy2 + opaque [id] + (with_strategy2 + opaque [id] + (assert_fails unfold_id; + with_strategy2 + transparent [id] + (assert_succeeds unfold_id; + with_strategy2 + opaque [id] + (with_strategy2 + 0 [id] + (assert_succeeds unfold_id; + with_strategy2 + 1 [id] + (assert_succeeds unfold_id; + with_strategy2 + -1 [id] + (assert_succeeds unfold_id; + with_strategy2 + opaque [id] + (assert_fails unfold_id; + with_strategy2 + transparent [id] + (assert_succeeds unfold_id; + with_strategy2 + opaque [id] + (with_strategy2 + expand [id] + (assert_succeeds unfold_id))))))))))). + (* This should succeed, but doesn't, basically due to https://github.com/coq/coq/issues/11202 *) + Fail let idx := smart_global:(id) in + with_strategy2 expand [idx] idtac. + reflexivity. +Qed. +Goal id 0 = 0. + with_strategy2 + opaque [aid] + (with_strategy2 + opaque [aid] + (assert_fails unfold_id; + with_strategy2 + transparent [aid] + (assert_succeeds unfold_id; + with_strategy2 + opaque [aid] + (with_strategy2 + 0 [aid] + (assert_succeeds unfold_id; + with_strategy2 + 1 [aid] + (assert_succeeds unfold_id; + with_strategy2 + -1 [aid] + (assert_succeeds unfold_id; + with_strategy2 + opaque [aid] + (assert_fails unfold_id; + with_strategy2 + transparent [aid] + (assert_succeeds unfold_id; + with_strategy2 + opaque [aid] + (with_strategy2 + expand [aid] + (assert_succeeds unfold_id))))))))))). + reflexivity. +Qed. +Goal id 0 = 0. + with_strategy2 + opaque [idn] + (with_strategy2 + opaque [idn] + (assert_fails unfold_id; + with_strategy2 + transparent [idn] + (assert_succeeds unfold_id; + with_strategy2 + opaque [idn] + (with_strategy2 + 0 [idn] + (assert_succeeds unfold_id; + with_strategy2 + 1 [idn] + (assert_succeeds unfold_id; + with_strategy2 + -1 [idn] + (assert_succeeds unfold_id; + with_strategy2 + opaque [idn] + (assert_fails unfold_id; + with_strategy2 + transparent [idn] + (assert_succeeds unfold_id; + with_strategy2 + opaque [idn] + (with_strategy2 + expand [idn] + (assert_succeeds unfold_id))))))))))). + reflexivity. +Qed. + +Opaque id. +Goal id 0 = 0. + with_strategy3 + opaque [id] + (with_strategy3 + opaque [id] + (assert_fails unfold_id; + with_strategy3 + transparent [id] + (assert_succeeds unfold_id; + with_strategy3 + opaque [id] + (with_strategy3 + 0 [id] + (assert_succeeds unfold_id; + with_strategy3 + 1 [id] + (assert_succeeds unfold_id; + with_strategy3 + -1 [id] + (assert_succeeds unfold_id; + with_strategy3 + opaque [id] + (assert_fails unfold_id; + with_strategy3 + transparent [id] + (assert_succeeds unfold_id; + with_strategy3 + opaque [id] + (with_strategy3 + expand [id] + (assert_succeeds unfold_id))))))))))). + (* This should succeed, but doesn't, basically due to https://github.com/coq/coq/issues/11202 *) + Fail let idx := smart_global:(id) in + with_strategy3 expand [idx] idtac. + reflexivity. +Qed. +Goal id 0 = 0. + with_strategy3 + opaque [aid] + (with_strategy3 + opaque [aid] + (assert_fails unfold_id; + with_strategy3 + transparent [aid] + (assert_succeeds unfold_id; + with_strategy3 + opaque [aid] + (with_strategy3 + 0 [aid] + (assert_succeeds unfold_id; + with_strategy3 + 1 [aid] + (assert_succeeds unfold_id; + with_strategy3 + -1 [aid] + (assert_succeeds unfold_id; + with_strategy3 + opaque [aid] + (assert_fails unfold_id; + with_strategy3 + transparent [aid] + (assert_succeeds unfold_id; + with_strategy3 + opaque [aid] + (with_strategy3 + expand [aid] + (assert_succeeds unfold_id))))))))))). + reflexivity. +Qed. +Goal id 0 = 0. + with_strategy3 + opaque [idn] + (with_strategy3 + opaque [idn] + (assert_fails unfold_id; + with_strategy3 + transparent [idn] + (assert_succeeds unfold_id; + with_strategy3 + opaque [idn] + (with_strategy3 + 0 [idn] + (assert_succeeds unfold_id; + with_strategy3 + 1 [idn] + (assert_succeeds unfold_id; + with_strategy3 + -1 [idn] + (assert_succeeds unfold_id; + with_strategy3 + opaque [idn] + (assert_fails unfold_id; + with_strategy3 + transparent [idn] + (assert_succeeds unfold_id; + with_strategy3 + opaque [idn] + (with_strategy3 + expand [idn] + (assert_succeeds unfold_id))))))))))). + reflexivity. +Qed. + +(* Fake out coqchk to work around what is essentially COQBUG(https://github.com/coq/coq/issues/12200) *) +Reset Initial. |