aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/CasesDep.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/success/CasesDep.v')
-rw-r--r--test-suite/success/CasesDep.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v
index 8d0dc0f5c..3313827f1 100644
--- a/test-suite/success/CasesDep.v
+++ b/test-suite/success/CasesDep.v
@@ -76,7 +76,7 @@ Grammar constr constr1 :=
Definition equal := [A:Setoid]
<[s:Setoid](Relation |s|)>let (S,R,e)=A in R.
-Grammar constr constr1 :=
+Grammar constr constr1 := NONA
equal [ constr0($c) "=" "%" "S" constr0($c2) ] ->
[ (equal ? $c $c2) ].
@@ -111,7 +111,7 @@ End Maps.
Notation ap := (explicit_ap ? ?).
-Grammar constr constr8 :=
+Grammar constr constr8 := RIGHTA
map_setoid [ constr7($c1) "=>" constr8($c2) ]
-> [ (Map_setoid $c1 $c2) ].