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.
---
 plugins/ssr/ssrvernac.ml4 | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 3efb7b9147..4f530a0aec 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 ->
-- 
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...
---
 plugins/funind/indfun_common.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'plugins')

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 8bf6e48fdb..5a9248d478 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
 
-- 
cgit v1.2.3