Merge PR #978: In printing, experimenting factorizing "match" clauses with same right-hand side.

21 files changed, 312 insertions, 46 deletions

diff --git a/API/API.mli b/API/API.mli
index f9231a15e..8f46a5832 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2394,7 +2394,7 @@ sig
    and case_expr = constr_expr * Names.Name.t Loc.located option * cases_pattern_expr option
 
    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 =
      Names.Name.t Loc.located list * binder_kind * constr_expr
@@ -4346,6 +4346,7 @@ sig
   | Later : [ `thunk ] delay
   val print_universes : bool ref
   val print_evar_arguments : bool ref
+  val print_allow_match_default_clause : bool ref
   val detype : 'a delay -> ?lax:bool -> bool -> Names.Id.Set.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> 'a Glob_term.glob_constr_g
   val subst_glob_constr : Mod_subst.substitution -> Glob_term.glob_constr -> Glob_term.glob_constr
   val set_detype_anonymous : (?loc:Loc.t -> int -> Names.Id.t) -> unit
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"
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 5c519e46e..a1950d136 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -550,6 +550,60 @@ the same way as the {\Coq} kernel handles them.
 This tells if the printing matching mode is on or off. The default is
 on.
 
+\subsubsection{Factorization of clauses with same right-hand side}
+\label{SetPrintingFactorizableMatchPatterns}
+\optindex{Printing Factorizable Match Patterns}
+
+When several patterns share the same right-hand side, it is
+additionally possible to share the clauses using disjunctive patterns.
+Assuming that the printing matching mode is on, whether {\Coq}'s
+printer shall try to do this kind of factorization is governed by the
+following commands:
+
+\begin{quote}
+{\tt Set Printing Factorizable Match Patterns.}
+\end{quote}
+This tells {\Coq}'s printer to try to use disjunctive patterns. This is the default
+behavior.
+
+\begin{quote}
+{\tt Unset Printing Factorizable Match Patterns.}
+\end{quote}
+This tells {\Coq}'s printer not to try to use disjunctive patterns.
+
+\begin{quote}
+{\tt Test Printing Factorizable Match Patterns.}
+\end{quote}
+This tells if the factorization of clauses with same right-hand side is
+on or off.
+
+\subsubsection{Use of a default clause}
+\label{SetPrintingAllowDefaultClause}
+\optindex{Printing Allow Default Clause}
+
+When several patterns share the same right-hand side which do not
+depend on the arguments of the patterns, yet an extra factorization is
+possible: the disjunction of patterns can be replaced with a ``{\tt
+  \_}'' default clause. Assuming that the printing matching mode and
+the factorization mode are on, whether {\Coq}'s printer shall try to
+use a default clause is governed by the following commands:
+
+\begin{quote}
+{\tt Set Printing Allow Default Clause.}
+\end{quote}
+This tells {\Coq}'s printer to use a default clause when relevant. This is the default
+behavior.
+
+\begin{quote}
+{\tt Unset Printing Allow Default Clause.}
+\end{quote}
+This tells {\Coq}'s printer not to use a default clause.
+
+\begin{quote}
+{\tt Test Printing Allow Default Clause.}
+\end{quote}
+This tells if the use of a default clause is allowed.
+
 \subsubsection{Printing of wildcard pattern
 \optindex{Printing Wildcard}}
 
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 8b78a91b5..7cc8de85d 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -188,7 +188,7 @@ and case_expr_eq (e1, n1, p1) (e2, n2, p2) =
   Option.equal cases_pattern_expr_eq p1 p2
 
 and branch_expr_eq (_, (p1, e1)) (_, (p2, e2)) =
-  List.equal (eq_located (List.equal cases_pattern_expr_eq)) p1 p2 &&
+  List.equal (List.equal cases_pattern_expr_eq) p1 p2 &&
   constr_expr_eq e1 e2
 
 and binder_expr_eq ((n1, _, e1) : binder_expr) (n2, _, e2) =
@@ -260,7 +260,6 @@ let local_binders_loc bll = match bll with
 
 (* Legacy functions *)
 let down_located f (_l, x) = f x
-let located_fold_left f x (_l, y) = f x y
 
 let is_constructor id =
   try Globnames.isConstructRef
@@ -292,8 +291,7 @@ let ids_of_pattern =
 
 let ids_of_pattern_list =
   List.fold_left
-    (located_fold_left
-       (List.fold_left (cases_pattern_fold_names Id.Set.add)))
+    (List.fold_left (cases_pattern_fold_names Id.Set.add))
     Id.Set.empty
 
 let ids_of_cases_indtype p =
@@ -571,7 +569,7 @@ let expand_binders ?loc mkC bl c =
         let c = CAst.make ?loc @@
           CCases
             (LetPatternStyle, None, [(e,None,None)],
-             [(Loc.tag ?loc:loc1 ([(loc1,[p])], c))])
+             [(Loc.tag ?loc:loc1 ([[p]], c))])
         in
         (ni :: env, mkC ?loc ([id],Default Explicit,ty) c)
   in
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index bc8debd02..1330b3741 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 ([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
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 977146b2f..74ae32120 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -958,8 +958,11 @@ let rec has_duplicate = function
   | [] -> None
   | x::l -> if Id.List.mem x l then (Some x) else has_duplicate l
 
+let loc_of_multiple_pattern pl =
+ Loc.merge_opt (cases_pattern_expr_loc (List.hd pl)) (cases_pattern_expr_loc (List.last pl))
+
 let loc_of_lhs lhs =
- Loc.merge_opt (fst (List.hd lhs)) (fst (List.last lhs))
+ Loc.merge_opt (loc_of_multiple_pattern (List.hd lhs)) (loc_of_multiple_pattern (List.last lhs))
 
 let check_linearity lhs ids =
   match has_duplicate ids with
@@ -1873,8 +1876,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
     intern_local_binder_aux intern ntnvars env bind
 
   (* Expands a multiple pattern into a disjunction of multiple patterns *)
-  and intern_multiple_pattern env n (loc,pl) =
+  and intern_multiple_pattern env n pl =
     let idsl_pll = List.map (intern_cases_pattern globalenv (None,env.scopes) empty_alias) pl in
+    let loc = loc_of_multiple_pattern pl in
     check_number_of_pattern loc n pl;
     product_of_cases_patterns empty_alias idsl_pll
 
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml
index e0d2d7bf4..8bcdbcc0e 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
diff --git a/intf/glob_term.ml b/intf/glob_term.ml
index 72c91db6a..f311d33b8 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
diff --git a/lib/pp.ml b/lib/pp.ml
index c3338688d..770e650cb 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -208,6 +208,7 @@ let string_of_ppcmds c =
 let pr_comma () = str "," ++ spc ()
 let pr_semicolon () = str ";" ++ spc ()
 let pr_bar () = str "|" ++ spc ()
+let pr_spcbar () = str " |" ++ spc ()
 let pr_arg pr x = spc () ++ pr x
 let pr_non_empty_arg pr x = let pp = pr x in if ismt pp then mt () else spc () ++ pr x
 let pr_opt pr = function None -> mt () | Some x -> pr_arg pr x
diff --git a/lib/pp.mli b/lib/pp.mli
index 2d11cad86..d9be1c5ce 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -120,6 +120,9 @@ val pr_semicolon : unit -> t
 val pr_bar : unit -> t
 (** Well-spaced pipe bar. *)
 
+val pr_spcbar : unit -> t
+(** Pipe bar with space before and after. *)
+
 val pr_arg : ('a -> t) -> 'a -> t
 (** Adds a space in front of its argument. *)
 
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 0cf96d487..db68a75e0 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -267,17 +267,17 @@ GEXTEND Gram
       | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
           "in"; c2 = operconstr LEVEL "200" ->
 	    CAst.make ~loc:!@loc @@
-            CCases (LetPatternStyle, None,    [c1, None, None],       [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)])
+            CCases (LetPatternStyle, None,    [c1, None, None],       [Loc.tag ~loc:!@loc ([[p]], c2)])
       | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
 	  rt = case_type; "in"; c2 = operconstr LEVEL "200" ->
 	    CAst.make ~loc:!@loc @@
-            CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)])
+            CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [Loc.tag ~loc:!@loc ([[p]], c2)])
 
       | "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200";
 	  ":="; c1 = operconstr LEVEL "200"; rt = case_type;
           "in"; c2 = operconstr LEVEL "200" ->
 	    CAst.make ~loc:!@loc @@
-            CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)])
+            CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [Loc.tag ~loc:!@loc ([[p]], c2)])
       | "if"; c=operconstr LEVEL "200"; po = return_type;
 	"then"; b1=operconstr LEVEL "200";
         "else"; b2=operconstr LEVEL "200" ->
@@ -362,7 +362,7 @@ GEXTEND Gram
     [ [ OPT"|"; br=LIST0 eqn SEP "|" -> br ] ]
   ;
   mult_pattern:
-    [ [ pl = LIST1 pattern LEVEL "99" SEP "," -> (Loc.tag ~loc:!@loc pl) ] ]
+    [ [ pl = LIST1 pattern LEVEL "99" SEP "," -> pl ] ]
   ;
   eqn:
     [ [ pll = LIST1 mult_pattern SEP "|";
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 8bf6e48fd..5a9248d47 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -183,7 +183,9 @@ let with_full_print f a =
   and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
   let old_rawprint = !Flags.raw_print in
   let old_printuniverses = !Constrextern.print_universes in
+  let old_printallowmatchdefaultclause = !Detyping.print_allow_match_default_clause in
   Constrextern.print_universes := true;
+  Detyping.print_allow_match_default_clause := false;
   Flags.raw_print := true;
   Impargs.make_implicit_args false;
   Impargs.make_strict_implicit_args false;
@@ -197,6 +199,7 @@ let with_full_print f a =
     Impargs.make_contextual_implicit_args old_contextual_implicit_args;
     Flags.raw_print := old_rawprint;
     Constrextern.print_universes := old_printuniverses;
+    Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause;
     Dumpglob.continue ();
     res
   with
@@ -206,6 +209,7 @@ let with_full_print f a =
 	Impargs.make_contextual_implicit_args old_contextual_implicit_args;
 	Flags.raw_print := old_rawprint;
 	Constrextern.print_universes := old_printuniverses;
+        Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause;
 	Dumpglob.continue ();
 	raise reraise
 
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 3efb7b914..4f530a0ae 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -74,7 +74,7 @@ let frozen_lexer = CLexer.get_keyword_state () ;;
 
 let no_ct = None, None and no_rt = None in 
 let aliasvar = function
-  | [_, [{ CAst.v = CPatAlias (_, id); loc }]] -> Some (loc,Name id)
+  | [[{ CAst.v = CPatAlias (_, id); loc }]] -> Some (loc,Name id)
   | _ -> None in
 let mk_cnotype mp = aliasvar mp, None in
 let mk_ctype mp t = aliasvar mp, Some t in
@@ -86,14 +86,14 @@ let mk_pat c (na, t) = (c, na, t) in
 GEXTEND Gram
   GLOBAL: binder_constr;
   ssr_rtype: [[ "return"; t = operconstr LEVEL "100" -> mk_rtype t ]];
-  ssr_mpat: [[ p = pattern -> [Loc.tag ~loc:!@loc [p]] ]];
+  ssr_mpat: [[ p = pattern -> [[p]] ]];
   ssr_dpat: [
     [ mp = ssr_mpat; "in"; t = pattern; rt = ssr_rtype -> mp, mk_ctype mp t, rt
     | mp = ssr_mpat; rt = ssr_rtype -> mp, mk_cnotype mp, rt
     | mp = ssr_mpat -> mp, no_ct, no_rt
   ] ];
   ssr_dthen: [[ dp = ssr_dpat; "then"; c = lconstr -> mk_dthen ~loc:!@loc dp c ]];
-  ssr_elsepat: [[ "else" -> [Loc.tag ~loc:!@loc [CAst.make ~loc:!@loc @@ CPatAtom None]] ]];
+  ssr_elsepat: [[ "else" -> [[CAst.make ~loc:!@loc @@ CPatAtom None]] ]];
   ssr_else: [[ mp = ssr_elsepat; c = lconstr -> Loc.tag ~loc:!@loc (mp, c) ]];
   binder_constr: [
     [ "if"; c = operconstr LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else ->
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 4f3669a2b..1207c967b 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1566,11 +1566,9 @@ substituer après par les initiaux *)
 
 (* builds the matrix of equations testing that each eqn has n patterns
  * and linearizing the _ patterns.
- * Syntactic correctness has already been done in astterm *)
+ * Syntactic correctness has already been done in constrintern *)
 let matx_of_eqns env eqns =
-  let build_eqn (loc,(ids,lpat,rhs)) =
-    let initial_lpat,initial_rhs = lpat,rhs in
-    let initial_rhs = rhs in
+  let build_eqn (loc,(ids,initial_lpat,initial_rhs)) =
     let avoid = ids_of_named_context_val (named_context_val env) in
     let avoid = List.fold_left (fun accu id -> Id.Set.add id accu) avoid ids in
     let rhs =
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 6527ba935..23993243f 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -252,6 +252,89 @@ let lookup_index_as_renamed env sigma t n =
   in lookup n 1 t
 
 (**********************************************************************)
+(* Factorization of match patterns *)
+
+let print_factorize_match_patterns = ref true
+
+let _ =
+  let open Goptions in
+  declare_bool_option
+    { optdepr  = false;
+      optname  = "factorization of \"match\" patterns in printing";
+      optkey   = ["Printing";"Factorizable";"Match";"Patterns"];
+      optread  = (fun () -> !print_factorize_match_patterns);
+      optwrite = (fun b -> print_factorize_match_patterns := b) }
+
+let print_allow_match_default_clause = ref true
+
+let _ =
+  let open Goptions in
+  declare_bool_option
+    { optdepr  = false;
+      optname  = "possible use of \"match\" default pattern in printing";
+      optkey   = ["Printing";"Allow";"Match";"Default";"Clause"];
+      optread  = (fun () -> !print_allow_match_default_clause);
+      optwrite = (fun b -> print_allow_match_default_clause := b) }
+
+let rec join_eqns (ids,rhs as x) patll = function
+  | (loc,(ids',patl',rhs') as eqn')::rest ->
+     if not !Flags.raw_print && !print_factorize_match_patterns &&
+        List.eq_set Id.equal ids ids' && glob_constr_eq rhs rhs'
+     then
+       join_eqns x (patl'::patll) rest
+     else
+       let eqn,rest = join_eqns x patll rest in
+       eqn, eqn'::rest
+  | [] ->
+     patll, []
+
+let number_of_patterns (_gloc,(_ids,patll,_rhs)) = List.length patll
+
+let is_default_candidate (_gloc,(ids,_patll,_rhs) ) = ids = []
+
+let rec move_more_factorized_default_candidate_to_end eqn n = function
+  | eqn' :: eqns ->
+     let set,get = set_temporary_memory () in
+     if is_default_candidate eqn' && set (number_of_patterns eqn') >= n then
+       let isbest, dft, eqns = move_more_factorized_default_candidate_to_end eqn' (get ()) eqns in
+       if isbest then false, dft, eqns else false, dft, eqn' :: eqns
+     else
+       let isbest, dft, eqns = move_more_factorized_default_candidate_to_end eqn n eqns in
+       isbest, dft, eqn' :: eqns
+  | [] -> true, Some eqn, []
+
+let rec select_default_clause = function
+  | eqn :: eqns ->
+     let set,get = set_temporary_memory () in
+     if is_default_candidate eqn && set (number_of_patterns eqn) > 1 then
+       let isbest, dft, eqns = move_more_factorized_default_candidate_to_end eqn (get ()) eqns in
+       if isbest then dft, eqns else dft, eqn :: eqns
+     else
+       let dft, eqns = select_default_clause eqns in dft, eqn :: eqns
+  | [] -> None, []
+
+let factorize_eqns eqns =
+  let rec aux found = function
+  | (loc,(ids,patl,rhs))::rest ->
+     let patll,rest = join_eqns (ids,rhs) [patl] rest in
+     aux ((loc,(ids,patll,rhs))::found) rest
+  | [] ->
+     found in
+  let eqns = aux [] (List.rev eqns) in
+  let mk_anon patl = List.map (fun _ -> DAst.make @@ PatVar Anonymous) patl in
+  if not !Flags.raw_print && !print_allow_match_default_clause && eqns <> [] then
+    match select_default_clause eqns with
+    (* At least two clauses and the last one is disjunctive with no variables *)
+    | Some (gloc,([],patl::_::_,rhs)), (_::_ as eqns) -> eqns@[gloc,([],[mk_anon patl],rhs)]
+    (* Only one clause which is disjunctive with no variables: we keep at least one constructor *)
+    (* so that it is not interpreted as a dummy "match" *)
+    | Some (gloc,([],patl::patl'::_,rhs)), [] -> [gloc,([],[patl;mk_anon patl'],rhs)]
+    | Some (_,((_::_,_,_ | _,([]|[_]),_))), _ -> assert false
+    | None, eqns -> eqns
+  else
+    eqns
+
+(**********************************************************************)
 (* Fragile algorithm to reverse pattern-matching compilation          *)
 
 let update_name sigma na ((_,(e,_)),c) =
@@ -284,13 +367,12 @@ let rec decomp_branch tags nal b (avoid,env as e) sigma c =
 let rec build_tree na isgoal e sigma ci cl =
   let mkpat n rhs pl = DAst.make @@ PatCstr((ci.ci_ind,n+1),pl,update_name sigma na rhs) in
   let cnl = ci.ci_pp_info.cstr_tags in
-  let cna = ci.ci_cstr_nargs in
   List.flatten
     (List.init (Array.length cl)
-      (fun i -> contract_branch isgoal e sigma (cnl.(i),cna.(i),mkpat i,cl.(i))))
+      (fun i -> contract_branch isgoal e sigma (cnl.(i),mkpat i,cl.(i))))
 
 and align_tree nal isgoal (e,c as rhs) sigma = match nal with
-  | [] -> [[],rhs]
+  | [] -> [Id.Set.empty,[],rhs]
   | na::nal ->
     match EConstr.kind sigma c with
     | Case (ci,p,c,cl) when
@@ -300,19 +382,20 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with
 	computable sigma p (List.length ci.ci_pp_info.ind_tags) (* FIXME: can do better *) ->
 	let clauses = build_tree na isgoal e sigma ci cl in
 	List.flatten
-          (List.map (fun (pat,rhs) ->
+          (List.map (fun (ids,pat,rhs) ->
 	      let lines = align_tree nal isgoal rhs sigma in
-	      List.map (fun (hd,rest) -> pat::hd,rest) lines)
+              List.map (fun (ids',hd,rest) -> Id.Set.fold Id.Set.add ids ids',pat::hd,rest) lines)
 	    clauses)
     | _ ->
-	let pat = DAst.make @@ PatVar(update_name sigma na rhs) in
-	let mat = align_tree nal isgoal rhs sigma in
-	List.map (fun (hd,rest) -> pat::hd,rest) mat
+        let na = update_name sigma na rhs in
+        let pat = DAst.make @@ PatVar na in
+        let mat = align_tree nal isgoal rhs sigma in
+        List.map (fun (ids,hd,rest) -> Nameops.Name.fold_right Id.Set.add na ids,pat::hd,rest) mat
 
-and contract_branch isgoal e sigma (cdn,can,mkpat,b) =
-  let nal,rhs = decomp_branch cdn [] isgoal e sigma b in
+and contract_branch isgoal e sigma (cdn,mkpat,rhs) =
+  let nal,rhs = decomp_branch cdn [] isgoal e sigma rhs in
   let mat = align_tree nal isgoal rhs sigma in
-  List.map (fun (hd,rhs) -> (mkpat rhs hd,rhs)) mat
+  List.map (fun (ids,hd,rhs) -> ids,mkpat rhs hd,rhs) mat
 
 (**********************************************************************)
 (* Transform internal representation of pattern-matching into list of *)
@@ -648,7 +731,7 @@ and detype_eqns d flags avoid env sigma ci computable constructs consnargsl bl =
   try
     if !Flags.raw_print || not (reverse_matching ()) then raise Exit;
     let mat = build_tree Anonymous (snd flags) (avoid,env) sigma ci bl in
-    List.map (fun (pat,((avoid,env),c)) -> Loc.tag ([],[pat],detype d flags avoid env sigma c))
+    List.map (fun (ids,pat,((avoid,env),c)) -> Loc.tag (Id.Set.elements ids,[pat],detype d flags avoid env sigma c))
       mat
   with e when CErrors.noncritical e ->
     Array.to_list
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index cb1c0d8d4..f150cb195 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -26,10 +26,20 @@ val print_universes : bool ref
 (** If true, prints full local context of evars *)
 val print_evar_arguments : bool ref
 
+(** If true, contract branches with same r.h.s. and same matching
+    variables in a disjunctive pattern *)
+val print_factorize_match_patterns : bool ref
+
+(** If true and the last non unique clause of a "match" is a
+    variable-free disjunctive pattern, turn it into a catch-call case *)
+val print_allow_match_default_clause : bool ref
+
 val subst_cases_pattern : substitution -> cases_pattern -> cases_pattern
 
 val subst_glob_constr : substitution -> glob_constr -> glob_constr
 
+val factorize_eqns : 'a cases_clauses_g -> 'a disjunctive_cases_clauses_g
+
 (** [detype isgoal avoid ctx c] turns a closed [c], into a glob_constr 
    de Bruijn indexes are turned to bound names, avoiding names in [avoid] 
    [isgoal] tells if naming must avoid global-level synonyms as intro does 
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 2abbc389f..51735bc9e 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -286,7 +286,7 @@ let tag_var = tag Tag.variable
         pr_reference r, latom
 
       | CPatOr pl ->
-        hov 0 (prlist_with_sep pr_bar (pr_patt spc (lpator,L)) pl), lpator
+        hov 0 (prlist_with_sep pr_spcbar (pr_patt mt (lpator,L)) pl), lpator
 
       | CPatNotation ("( _ )",([p],[]),[]) ->
         pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom
@@ -311,11 +311,10 @@ let tag_var = tag Tag.variable
   let pr_patt = pr_patt mt
 
   let pr_eqn pr (loc,(pl,rhs)) =
-    let pl = List.map snd pl in
     spc() ++ hov 4
       (pr_with_comments ?loc
          (str "| " ++
-            hov 0 (prlist_with_sep pr_bar (prlist_with_sep sep_v (pr_patt ltop)) pl
+            hov 0 (prlist_with_sep pr_spcbar (prlist_with_sep sep_v (pr_patt ltop)) pl
                    ++ str " =>") ++
             pr_sep_com spc (pr ltop) rhs))
 
@@ -402,7 +401,7 @@ let tag_var = tag Tag.variable
     | { v = CProdN ([],c) } ->
       extract_prod_binders c
     | { loc; v = CProdN ([[_,Name id],bk,t],
-              { v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([_,[p]],b))])} ) }
+              { v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([[p]],b))])} ) }
          when Id.equal id id' && not (Id.Set.mem id (free_vars_of_constr_expr b)) ->
       let bl,c = extract_prod_binders b in
       CLocalPattern (loc, (p,None)) :: bl, c
@@ -418,7 +417,7 @@ let tag_var = tag Tag.variable
     | CLambdaN ([],c) ->
       extract_lam_binders c
     | CLambdaN ([[_,Name id],bk,t],
-                { v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([_,[p]],b))])} )
+                { v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([[p]],b))])} )
          when Id.equal id id' && not (Id.Set.mem id (free_vars_of_constr_expr b)) ->
       let bl,c = extract_lam_binders b in
       CLocalPattern (ce.loc,(p,None)) :: bl, c
@@ -650,7 +649,7 @@ let tag_var = tag Tag.variable
           hv 0 (str"{|" ++ pr_record_body_gen (pr spc) l ++ str" |}"),
           latom
         )
-      | CCases (LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[(_,([(loc,[p])],b))]) ->
+      | CCases (LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[(_,([[p]],b))]) ->
         return (
           hv 0 (
             keyword "let" ++ spc () ++ str"'" ++
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 97fa8e254..419dcadb4 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -95,8 +95,7 @@ fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
   
   x : nat
   n, n0 := match x + 0 with
-           | 0 => 0
-           | S _ => 0
+           | 0 | S _ => 0
            end : nat
   e,
   e0 := match x + 0 as y return (y = y) with
@@ -104,8 +103,7 @@ fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
         | S n => eq_refl
         end : x + 0 = x + 0
   n1, n2 := match x with
-            | 0 => 0
-            | S _ => 0
+            | 0 | S _ => 0
             end : nat
   e1, e2 := match x return (x = x) with
             | 0 => eq_refl
@@ -126,3 +124,48 @@ fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
         end : p = p /\ p = p
   ============================
   eq_refl = eq_refl
+fun x : comparison => match x with
+                      | Eq => 1
+                      | _ => 0
+                      end
+     : comparison -> nat
+fun x : comparison => match x with
+                      | Eq => 1
+                      | Lt => 0
+                      | Gt => 0
+                      end
+     : comparison -> nat
+fun x : comparison => match x with
+                      | Eq => 1
+                      | Lt | Gt => 0
+                      end
+     : comparison -> nat
+fun x : comparison =>
+match x return nat with
+| Eq => S O
+| Lt => O
+| Gt => O
+end
+     : forall _ : comparison, nat
+fun x : K => match x with
+             | a3 | a4 => 3
+             | _ => 2
+             end
+     : K -> nat
+fun x : K => match x with
+             | a1 | a2 => 4
+             | a3 => 3
+             | _ => 2
+             end
+     : K -> nat
+fun x : K => match x with
+             | a1 | a2 => 4
+             | a4 => 3
+             | _ => 2
+             end
+     : K -> nat
+fun x : K => match x with
+             | a1 | a3 | a4 => 3
+             | _ => 2
+             end
+     : K -> nat
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 17fee3303..caf3b2870 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -1,5 +1,7 @@
 (* Cases with let-in in constructors types *)
 
+Unset Printing Allow Match Default Clause.
+
 Inductive t : Set :=
     k : let x := t in x -> x.
 
@@ -184,3 +186,33 @@ let p := fresh "p" in
   |- eq_refl ?p = _ => pose (match eq_refl p in _ = z return p=p /\ z=z with eq_refl => conj eq_refl eq_refl end)
   end.
 Show.
+
+Set Printing Allow Match Default Clause.
+
+(***************************************************)
+(* Testing strategy for factorizing cases branches *)
+
+(* Factorization + default clause *)
+Check fun x => match x with Eq => 1 | _ => 0 end.
+
+(* No factorization *)
+Unset Printing Factorizable Match Patterns.
+Check fun x => match x with Eq => 1 | _ => 0 end.
+Set Printing Factorizable Match Patterns.
+
+(* Factorization but no default clause *)
+Unset Printing Allow Match Default Clause.
+Check fun x => match x with Eq => 1 | _ => 0 end.
+Set Printing Allow Match Default Clause.
+
+(* No factorization in printing all mode *)
+Set Printing All.
+Check fun x => match x with Eq => 1 | _ => 0 end.
+Unset Printing All.
+
+(* Several clauses *)
+Inductive K := a1|a2|a3|a4|a5|a6.
+Check fun x => match x with a3 | a4 => 3 | _ => 2 end.
+Check fun x => match x with a3 => 3 | a2 | a1 => 4 | _ => 2 end.
+Check fun x => match x with a4 => 3 | a2 | a1 => 4 | _ => 2 end.
+Check fun x => match x with a3 | a4 | a1 => 3 | _ => 2 end.
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index a1028bda0..121a369a9 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -37,6 +37,17 @@ let' f (x y : nat) (a := 0) (z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2
 λ (f : nat -> nat) (x : nat), f(x) + S(x)
      : (nat -> nat) -> nat -> nat
 Notation plus2 n := (S(S(n)))
+λ n : list(nat), match n with
+                 | 1 :: nil => 0
+                 | _ => 2
+                 end
+     : list(nat) -> nat
+λ n : list(nat),
+match n with
+| 1 :: nil => 0
+| nil | 0 :: _ | 1 :: _ :: _ | plus2 _ :: _ => 2
+end
+     : list(nat) -> nat
 λ n : list(nat),
 match n with
 | nil => 2
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 4c3eaa0c7..531398bb0 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -79,6 +79,13 @@ Notation plus2 n := (S (S n)).
 (* plus2 was not correctly printed in the two following tests in 8.3pl1 *)
 Print plus2.
 Check fun n => match n with list1 => 0 | _ => 2 end.
+Unset Printing Allow Match Default Clause.
+Check fun n => match n with list1 => 0 | _ => 2 end.
+Unset Printing Factorizable Match Patterns.
+Check fun n => match n with list1 => 0 | _ => 2 end.
+Set Printing Allow Match Default Clause.
+Set Printing Factorizable Match Patterns.
+
 End A.
 
 (* This one is not fully satisfactory because binders in the same type