Failing testsuite item

Author: CohenCyril

_CoqProject.test-suite

@@ -94,6 +94,7 @@ tests/unit/mixin_src_has_mixin_instance.v
 tests/unit/mk_src_map.v
 tests/unit/close_hole_term.v
 tests/unit/struct.v
+tests/factory_when_notation.v
 
 -R tests HB.tests
 -R examples HB.examples

tests/factory_when_notation.v

@@ -0,0 +1,7 @@
+From HB Require Import structures.
+Notation x := (fun x : nat => true).
+HB.mixin Record m T := {x : T}.
+HB.factory Record f T := { x : T }.
+HB.builders Context T of f T.
+HB.instance Definition _ := m.Build T x.
+HB.end.