diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/5198.v | 39 | ||||
| -rw-r--r-- | test-suite/bugs/closed/5203.v | 5 | ||||
| -rw-r--r-- | test-suite/success/Typeclasses.v | 46 | ||||
| -rw-r--r-- | test-suite/success/bteauto.v | 6 |
4 files changed, 87 insertions, 9 deletions
diff --git a/test-suite/bugs/closed/5198.v b/test-suite/bugs/closed/5198.v new file mode 100644 index 000000000..7254afb42 --- /dev/null +++ b/test-suite/bugs/closed/5198.v @@ -0,0 +1,39 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-boot" "-nois") -*- *) +(* File reduced by coq-bug-finder from original input, then from 286 lines to +27 lines, then from 224 lines to 53 lines, then from 218 lines to 56 lines, +then from 269 lines to 180 lines, then from 132 lines to 48 lines, then from +253 lines to 65 lines, then from 79 lines to 65 lines *) +(* coqc version 8.6.0 (November 2016) compiled on Nov 12 2016 14:43:52 with +OCaml 4.02.3 + coqtop version jgross-Leopard-WS:/home/jgross/Downloads/coq/coq-v8.6,v8.6 +(7e992fa784ee6fa48af8a2e461385c094985587d) *) +Axiom admit : forall {T}, T. +Set Printing Implicit. +Inductive nat := O | S (_ : nat). +Axiom f : forall (_ _ : nat), nat. +Class ZLikeOps (e : nat) + := { LargeT : Type ; SmallT : Type ; CarryAdd : forall (_ _ : LargeT), LargeT +}. +Class BarrettParameters := + { b : nat ; k : nat ; ops : ZLikeOps (f b k) }. +Axiom barrett_reduce_function_bundled : forall {params : BarrettParameters} + (_ : @LargeT _ (@ops params)), + @SmallT _ (@ops params). + +Global Instance ZZLikeOps e : ZLikeOps (f (S O) e) + := { LargeT := nat ; SmallT := nat ; CarryAdd x y := y }. +Definition SRep := nat. +Local Instance x86_25519_Barrett : BarrettParameters + := { b := S O ; k := O ; ops := ZZLikeOps O }. +Definition SRepAdd : forall (_ _ : SRep), SRep + := let v := (fun x y => barrett_reduce_function_bundled (CarryAdd x y)) in + v. +Definition SRepAdd' : forall (_ _ : SRep), SRep + := (fun x y => barrett_reduce_function_bundled (CarryAdd x y)). +(* Error: +In environment +x : SRep +y : SRep +The term "x" has type "SRep" while it is expected to have type + "@LargeT ?e ?ZLikeOps". + *) diff --git a/test-suite/bugs/closed/5203.v b/test-suite/bugs/closed/5203.v new file mode 100644 index 000000000..ed137395f --- /dev/null +++ b/test-suite/bugs/closed/5203.v @@ -0,0 +1,5 @@ +Goal True. + Typeclasses eauto := debug. + Fail solve [ typeclasses eauto ]. + Fail typeclasses eauto. +
\ No newline at end of file diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index 5557ba837..f62427ef4 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -1,15 +1,28 @@ Module onlyclasses. +(* In 8.6 we still allow non-class subgoals *) Variable Foo : Type. Variable foo : Foo. Hint Extern 0 Foo => exact foo : typeclass_instances. Goal Foo * Foo. split. shelve. Set Typeclasses Debug. - Fail (unshelve typeclasses eauto); fail. - typeclasses eauto with typeclass_instances. - Unshelve. typeclasses eauto with typeclass_instances. + typeclasses eauto. + Unshelve. typeclasses eauto. Qed. + + Module RJung. + Class Foo (x : nat). + + Instance foo x : x = 2 -> Foo x. + Hint Extern 0 (_ = _) => reflexivity : typeclass_instances. + Typeclasses eauto := debug. + Check (_ : Foo 2). + + + Fail Definition foo := (_ : 0 = 0). + + End RJung. End onlyclasses. Module shelve_non_class_subgoals. @@ -17,16 +30,36 @@ Module shelve_non_class_subgoals. Variable foo : Foo. Hint Extern 0 Foo => exact foo : typeclass_instances. Class Bar := {}. - Instance bar1 (f:Foo) : Bar. + Instance bar1 (f:Foo) : Bar := {}. Typeclasses eauto := debug. Set Typeclasses Debug Verbosity 2. Goal Bar. (* Solution has shelved subgoals (of non typeclass type) *) - Fail typeclasses eauto. + typeclasses eauto. Abort. End shelve_non_class_subgoals. +Module RefineVsNoTceauto. + + Class Foo (A : Type) := foo : A. + Instance: Foo nat := { foo := 0 }. + Instance: Foo nat := { foo := 42 }. + Hint Extern 0 (_ = _) => refine eq_refl : typeclass_instances. + Goal exists (f : Foo nat), @foo _ f = 0. + Proof. + unshelve (notypeclasses refine (ex_intro _ _ _)). + Set Typeclasses Debug. Set Printing All. + all:once (typeclasses eauto). + Fail idtac. (* Check no subgoals are left *) + Undo 3. + (** In this case, the (_ = _) subgoal is not considered + by typeclass resolution *) + refine (ex_intro _ _ _). Fail reflexivity. + Abort. + +End RefineVsNoTceauto. + Module Leivantex2PR339. (** Was a bug preventing to find hints associated with no pattern *) Class Bar := {}. @@ -34,8 +67,9 @@ Module Leivantex2PR339. Hint Extern 0 => exact True : typeclass_instances. Typeclasses eauto := debug. Goal Bar. - Fail typeclasses eauto. Set Typeclasses Debug Verbosity 2. + typeclasses eauto. (* Relies on resolution of a non-class subgoal *) + Undo 1. typeclasses eauto with typeclass_instances. Qed. End Leivantex2PR339. diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v index 0af367781..3178c6fc1 100644 --- a/test-suite/success/bteauto.v +++ b/test-suite/success/bteauto.v @@ -24,9 +24,9 @@ Module Backtracking. Fail all:((once (typeclasses eauto with typeclass_instances)) + apply eq_refl). (* Does backtrack if other goals fail *) - all:[> (unshelve typeclasses eauto; fail) + reflexivity .. ]. + all:[> typeclasses eauto + reflexivity .. ]. Undo 1. - all:((unshelve typeclasses eauto; fail) + reflexivity). (* Note "+" is a focussing combinator *) + all:(typeclasses eauto + reflexivity). (* Note "+" is a focussing combinator *) Show Proof. Qed. @@ -66,7 +66,7 @@ Module Backtracking. unshelve evar (t : A). all:cycle 1. refine (@ex_intro _ _ t _). all:cycle 1. - all:((unshelve typeclasses eauto; fail) + reflexivity). + all:(typeclasses eauto + reflexivity). Qed. End Leivant. End Backtracking. |