While we don't have a clean alternative to Clenvtac, add a primitive

for tclEVARS which might solve existing goals.

1 files changed, 9 insertions, 0 deletions

diff --git a/test-suite/typeclasses/deftwice.v b/test-suite/typeclasses/deftwice.v
new file mode 100644
index 000000000..439782c9e
--- /dev/null
+++ b/test-suite/typeclasses/deftwice.v
@@ -0,0 +1,9 @@
+Class C (A : Type) := c : A -> Type.
+
+Record Inhab (A : Type) := { witness : A }. 
+
+Instance inhab_C : C Type := Inhab.
+
+Variable full : forall A (X : C A), forall x : A, c x.
+
+Definition truc {A : Type} : Inhab A := (full _ _ _).
\ No newline at end of file