push context in coq.ltac.open before collecting goals

Author: Tragicus

elpi/elpi-ltac.elpi

@@ -87,10 +87,10 @@ open T (nabla G) O :- (pi x\ open T (G x) (NG x)), private.distribute-nabla NG O
 open _ (seal (goal _ _ _ Solution _)) [] :- not (var Solution), !. % solved by side effect
 open T (seal (goal Ctx _ _ _ _ as G)) O :-
   std.filter Ctx private.not-already-assumed Ctx1,
-  (Ctx1 => T G O),
-  if (var O)
-     (G = goal _ _ _ P _, coq.ltac.collect-goals P O1 O2, std.append O1 O2 O)
-     true.
+  Ctx1 => (T G O,
+    if (var O)
+       (G = goal _ _ _ P _, coq.ltac.collect-goals P O1 O2, std.append O1 O2 O)
+       true).
 
 % helper code ---------------------------------------------------------------
 
@@ -127,4 +127,4 @@ func not-already-assumed prop.
 not-already-assumed (decl X _ _Ty) :- not(decl X _ _ ; def X _ _ _).
 not-already-assumed (def X _ _Ty _Bo) :- not(decl X _ _ ; def X _ _ _).
 
-}}
+}}