diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/modules/sub_objects.v | 2 | ||||
| -rw-r--r-- | test-suite/success/CasesDep.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/modules/sub_objects.v b/test-suite/modules/sub_objects.v index 73fd6f322c..2dbac34074 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). diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v index 5dd687859f..8d0dc0f5ca 100644 --- a/test-suite/success/CasesDep.v +++ b/test-suite/success/CasesDep.v @@ -109,7 +109,7 @@ Definition Map_setoid := (Build_Setoid Map ext Equiv_map_eq). End Maps. -Syntactic Definition ap := (explicit_ap ? ?). +Notation ap := (explicit_ap ? ?). Grammar constr constr8 := map_setoid [ constr7($c1) "=>" constr8($c2) ] |