Pass the test

toku-sa-n · Aug 12, 2023 · 90612f6 · 90612f6
1 parent 22ce0ed
commit 90612f6
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/lib/ppast.ml b/lib/ppast.ml
@@ -342,6 +342,9 @@ let pp_raw_atomic_tactic_expr printer (expr : Tacexpr.raw_atomic_tactic_expr) =
       write printer "destruct ";
       pp_induction_clause_list printer clause_list;
       write printer "."
+  | Tacexpr.TacIntroPattern
+      (false, [ CAst.{ v = Tactypes.IntroForthcoming _; loc = _ } ]) ->
+      write printer "intros."
   | Tacexpr.TacIntroPattern (false, exprs) ->
       write printer "intros ";
       spaced printer (fun expr -> pp_intro_pattern_expr printer expr.v) exprs;