1 files changed, 1 insertions, 1 deletions
diff --git a/syntax/PPConstr.v b/syntax/PPConstr.v
index 51ab2d5176..4980afd587 100755
--- a/syntax/PPConstr.v
+++ b/syntax/PPConstr.v
@@ -45,7 +45,7 @@ Syntax constr
 
 (* Things parsed in command1 *)
   level 1:
-    soap [(XTRA "$SOAPP" $lc1 ($LIST $cl))]
+    soap [(SOAPP $lc1 ($LIST $cl))]
       -> [ [<hov 0> "(" $lc1 ")@[" (NECOMMANDLIST ($LIST $cl)) "]"] ]
   | let_K [(ABST #Core#let.cci $M [<>]$N)]
       -> [ [<hov 0> "[_=" $M "]" [0 1] $N:E ] ]