doc/rationale.md

@@ -24,7 +24,7 @@ The name Pantograph is a pun. It means two things
   a locomotive. In comparison the (relatively) simple Pantograph software powers
   theorem proving projects.
 
-## Caveats and Limitations
+## Caveats
 
 Pantograph does not exactly mimic Lean LSP's behaviour. That would not grant the
 flexibility it offers.  To support tree search means Pantograph has to act
@@ -38,20 +38,7 @@ differently from Lean in some times, but never at the sacrifice of soundness.
   it is supposed to finish at the end of a `by` block. Pantograph will raise the
   error in this case, since it indicates the termination of a proof search branch.
 - `pick_goal` or `swap` will not work since they run contrary to tree search
-  paradigms. However, if there are tactics which perform non-trivial operations
-  to multiple goals at the same time, this constrain could potentially be
-  relaxed at a cost of great bookkeeping overhead to the user.
-
-Pantograph cannot perform things that are inherently constrained by Lean. These
-include:
-
-- If a tactic loses track of metavariables, it will not be caught until the end
-  of the proof search. This is a bug in the tactic itself.
-- Timeouts for executing tactics is not available. Maybe this will change in the
-  future.
-- Interceptions of parsing errors generally cannot be turned into goals (e.g.
-  `def mystery : Nat := :=`) due to Lean's parsing system.
-
+  paradigms.
 
 ## References