From c1cab3ba606f7034f2785f06c0d3892bca3976cf Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 18 Aug 2017 11:36:05 +0200
Subject: Removing cumbersome location in multiple patterns.

This is to have a better symmetry between CCases and GCases.
---
 intf/constrexpr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml
index e0d2d7bf48..8bcdbcc0ef 100644
--- a/intf/constrexpr.ml
+++ b/intf/constrexpr.ml
@@ -104,7 +104,7 @@ and case_expr = constr_expr                 (* expression that is being matched
 	      * cases_pattern_expr option   (* in-clause *)
 
 and branch_expr =
-  (cases_pattern_expr list Loc.located list * constr_expr) Loc.located
+  (cases_pattern_expr list list * constr_expr) Loc.located
 
 and binder_expr =
   Name.t Loc.located list * binder_kind * constr_expr
-- 
cgit v1.2.3


From 5c9d569cee804c099c44286777ab084e0370399f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 15 Aug 2017 14:51:08 +0200
Subject: 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...
---
 intf/glob_term.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'intf')

diff --git a/intf/glob_term.ml b/intf/glob_term.ml
index 72c91db6a0..f311d33b8a 100644
--- a/intf/glob_term.ml
+++ b/intf/glob_term.ml
@@ -93,6 +93,14 @@ type fix_recursion_order = [ `any ] fix_recursion_order_g
 
 type any_glob_constr = AnyGlobConstr : 'r glob_constr_g -> any_glob_constr
 
+type 'a disjunctive_cases_clause_g = (Id.t list * 'a cases_pattern_g list list * 'a glob_constr_g) Loc.located
+type 'a disjunctive_cases_clauses_g = 'a disjunctive_cases_clause_g list
+type 'a cases_pattern_disjunction_g = 'a cases_pattern_g list
+
+type disjunctive_cases_clause = [ `any ] disjunctive_cases_clause_g
+type disjunctive_cases_clauses = [ `any ] disjunctive_cases_clauses_g
+type cases_pattern_disjunction = [ `any ] cases_pattern_disjunction_g
+
 type 'a extended_glob_local_binder_r =
   | GLocalAssum   of Name.t * binding_kind * 'a glob_constr_g
   | GLocalDef     of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g option
-- 
cgit v1.2.3