@@ -878,7 +878,9 @@ pi syn =
878 (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing []]))) xt sc)) <|> (do
878 (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing []]))) xt sc)) <|> (do
879 try (lchar '{' *> reserved "default")
879 try (lchar '{' *> reserved "default")
880 when (st == Static) $ fail "default tactic constraints can not be static"
880 when (st == Static) $ fail "default tactic constraints can not be static"
881− script <- simpleExpr syn
882+ script' <- simpleExpr syn
883+ let script = debindApp syn . desugar syn ist $ script'
882 xt <- typeDeclList syn
884 xt <- typeDeclList syn
883 lchar '}'
885 lchar '}'
884 symbol "->"
886 symbol "->"