In printing, factorizing "match" clauses with same right-hand side.

Moreover, when there are at least two clauses and the last most
factorizable one is a disjunction with no variables, turn it into a
catch-all clause.

Adding options

  Unset Printing Allow Default Clause.

to deactivate the second behavior, and

  Unset Printing Factorizable Match Patterns.

to deactivate the first behavior (deactivating the first one
deactivates also the second one).

E.g. printing

  match x with Eq => 1 | _ => 0 end

gives

  match x with
  | Eq => 1
  | _ => 0
  end

or (with default clause deactivates):

  match x with
  | Eq => 1
  | Lt | Gt => 0
  end

More to be done, e.g. reconstructing multiple patterns in Nat.eqb...

1 files changed, 4 insertions, 4 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 6704ed4b7b..1330b3741e 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -852,7 +852,7 @@ let rec extern inctx scopes vars r =
                              ) x))
                 tml
     in
-    let eqns = List.map (extern_eqn inctx scopes vars) eqns in
+    let eqns = List.map (extern_eqn inctx scopes vars) (factorize_eqns eqns) in
     CCases (sty,rtntypopt',tml,eqns)
 
   | GLetTuple (nal,(na,typopt),tm,b) ->
@@ -966,9 +966,9 @@ and extern_local_binder scopes vars = function
       let (assums,ids,l) = extern_local_binder scopes vars l in
       (assums,ids, CLocalPattern(Loc.tag @@ (p,ty)) :: l)
 
-and extern_eqn inctx scopes vars (loc,(ids,pl,c)) =
-  Loc.tag ?loc ([List.map (extern_cases_pattern_in_scope scopes vars) pl],
-   extern inctx scopes vars c)
+and extern_eqn inctx scopes vars (loc,(ids,pll,c)) =
+  let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in
+  Loc.tag ?loc (pll,extern inctx scopes vars c)
 
 and extern_notation (tmp_scope,scopes as allscopes) vars t = function
   | [] -> raise No_match