aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/success')
-rw-r--r--test-suite/success/CasesDep.v2
1 files changed, 1 insertions, 1 deletions
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) ]