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, 10 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index b2b9da8ce..2b057f363 100644
--- a/CHANGES
+++ b/CHANGES
@@ -12,6 +12,16 @@ Notations
   opened rather than to the latest notations defined independently of
   whether they are in an opened scope or not.
 
+Specification language
+
+- When printing clauses of a "match", clauses with same right-hand
+  side are factorized and the last most factorized clause with no
+  variables, if it exists, is turned into a default clause.
+  Use "Unset Printing Allow Default Clause" do deactivate printing
+  of a default clause.
+  Use "Unset Printing Factorizable Match Patterns" to deactivate
+  factorization of clauses with same right-hand side.
+
 Tactics
 
 - On Linux, "native_compute" calls can be profiled using the "perf"