diff options
author | 2017-05-11 13:06:47 +0200 | |
---|---|---|
committer | 2017-05-11 13:06:47 +0200 | |
commit | e302b4dbc88c5776155c770aa90134edb571b738 (patch) | |
tree | cbb6d8a40f7e1baa30ce4968589b82b90b63b891 /test-suite/success | |
parent | a1788978360bd276bef721963e7adc47c1a49881 (diff) | |
parent | e4262a89d7bc3d9b985d9a4a939f34176581abcb (diff) |
Merge PR#201: Transparent abstract
Diffstat (limited to 'test-suite/success')
-rw-r--r-- | test-suite/success/transparent_abstract.v | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/test-suite/success/transparent_abstract.v b/test-suite/success/transparent_abstract.v new file mode 100644 index 000000000..ff4509c4a --- /dev/null +++ b/test-suite/success/transparent_abstract.v @@ -0,0 +1,21 @@ +Class by_transparent_abstract {T} (x : T) := make_by_transparent_abstract : T. +Hint Extern 0 (@by_transparent_abstract ?T ?x) => change T; transparent_abstract exact_no_check x : typeclass_instances. + +Goal True /\ True. +Proof. + split. + transparent_abstract exact I using foo. + let x := (eval hnf in foo) in constr_eq x I. + let x := constr:(ltac:(constructor) : True) in + let T := type of x in + let x := constr:(_ : by_transparent_abstract x) in + let x := (eval cbv delta [by_transparent_abstract] in (let y : T := x in y)) in + pose x as x'. + simpl in x'. + let v := eval cbv [x'] in x' in tryif constr_eq v I then fail 0 else idtac. + hnf in x'. + let v := eval cbv [x'] in x' in tryif constr_eq v I then idtac else fail 0. + exact x'. +Defined. +Check eq_refl : I = foo. +Eval compute in foo. |