From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- test-suite/success/transparent_abstract.v | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) create mode 100644 test-suite/success/transparent_abstract.v (limited to 'test-suite/success/transparent_abstract.v') diff --git a/test-suite/success/transparent_abstract.v b/test-suite/success/transparent_abstract.v new file mode 100644 index 00000000..ff4509c4 --- /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. -- cgit v1.2.3