Pp matches with or-patterns (#93)

toku-sa-n · Aug 12, 2023 · f0f0aa5 · f0f0aa5
1 parent ae65e54
commit f0f0aa5
Show file tree

Hide file tree

Showing 3 changed files with 22 additions and 3 deletions.
diff --git a/lib/ppast.ml b/lib/ppast.ml
@@ -164,12 +164,14 @@ and pp_local_binder_expr printer = function
   | _ -> raise (NotImplemented (contents printer))
 
 and pp_branch_expr printer = function
-  | CAst.{ v = [ patterns ], expr; loc = _ } ->
+  | CAst.{ v = patterns, expr; loc = _ } ->
       write printer "| ";
-      commad printer (pp_cases_pattern_expr printer) patterns;
+      with_seps
+        ~sep:(fun () -> write printer " | ")
+        (commad printer (pp_cases_pattern_expr printer))
+        patterns;
       write printer " => ";
       pp_constr_expr printer expr
-  | _ -> raise (NotImplemented (contents printer))
 
 let pp_definition_expr printer = function
   | Vernacexpr.ProveBody ([], expr) ->

diff --git a/test/coq_files/match/or-pattern/in.v b/test/coq_files/match/or-pattern/in.v
@@ -0,0 +1,3 @@
+Inductive foo:Type:=A|B|C|D|E|F.
+
+Definition bar(x:foo):nat:=match x with A=>1|B|C=>2|D|E|F=>3 end.
diff --git a/test/coq_files/match/or-pattern/out.v b/test/coq_files/match/or-pattern/out.v
@@ -0,0 +1,14 @@
+Inductive foo : Type :=
+  | A
+  | B
+  | C
+  | D
+  | E
+  | F.
+
+Definition bar (x : foo) : nat :=
+  match x with
+  | A => 1
+  | B | C => 2
+  | D | E | F => 3
+  end.