aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/modules
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/modules')
-rw-r--r--test-suite/modules/sub_objects.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/modules/sub_objects.v b/test-suite/modules/sub_objects.v
index 73fd6f322..2dbac3407 100644
--- a/test-suite/modules/sub_objects.v
+++ b/test-suite/modules/sub_objects.v
@@ -14,7 +14,7 @@ Module M.
Definition idid:=[A:Set][x:A](id x).
Grammar constr constr8 :=
not_eq [ "#" constr7($b) ] -> [ (idid $b) ].
- Syntactic Definition inc := (plus (S O)).
+ Notation inc := (plus (S O)).
End N.
Definition zero:=(N.idid O).