aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-03-03 21:35:42 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-03-03 21:35:42 +0100
commit7461aaedef508570fba6334e18fd10d5b32bda0e (patch)
tree5447b9e5003540af6144da269347cb76ef95125c
parent508d5a99101097948b6de342295eec0d5c8cbe72 (diff)
Adding a test for the behaviour of open_constr described in #3777.
-rw-r--r--test-suite/typeclasses/open_constr.v12
1 files changed, 12 insertions, 0 deletions
diff --git a/test-suite/typeclasses/open_constr.v b/test-suite/typeclasses/open_constr.v
new file mode 100644
index 000000000..5f1785c70
--- /dev/null
+++ b/test-suite/typeclasses/open_constr.v
@@ -0,0 +1,12 @@
+Tactic Notation "opose" open_constr(foo) := pose foo.
+Class Foo := Build_Foo : Set.
+Axiom f : forall `{Foo}, Set.
+Set Printing Implicit.
+Goal forall `{Foo}, True.
+Proof.
+ intro H.
+ pose f.
+ opose f.
+ Fail let x := (eval hnf in P) in has_evar x.
+ let x := (eval hnf in P0) in has_evar x.
+