From 1a43fda0dc9bb8d100808426980446353f8f1ae3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Apr 2017 11:21:23 +0200
Subject: Removing internal support for accepting "{struct x}" and co in
 "Theorem with".

There were actually no syntax for it, and I'm still unsure what good
syntax to give to it, even more that it would be useful to have one.
---
 printing/ppvernac.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index cfc2e48d11..d3b4007fbe 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -386,13 +386,12 @@ open Decl_kinds
     ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr def) def
     ++ prlist (pr_decl_notation pr_constr) ntn
 
-  let pr_statement head (idpl,(bl,c,guard)) =
+  let pr_statement head (idpl,(bl,c)) =
     assert (not (Option.is_empty idpl));
     let id, pl = Option.get idpl in
     hov 2
       (head ++ spc() ++ pr_lident id ++ pr_univs pl ++ spc() ++
          (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
-         pr_opt (pr_guard_annot pr_lconstr_expr bl) guard ++
          str":" ++ pr_spc_lconstr c)
 
   let pr_priority = function
-- 
cgit v1.2.3


From 02d2f34e5c84f0169e884c07054a6fbfef9f365c Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:04:58 +0200
Subject: Remove some unused values and types

---
 printing/ppconstr.ml | 4 ----
 printing/ppvernac.ml | 4 ----
 printing/printer.ml  | 5 -----
 3 files changed, 13 deletions(-)

(limited to 'printing')

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 38eeda9b96..3041ac259e 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -212,10 +212,6 @@ let tag_var = tag Tag.variable
       | Some (_,ExplByName id) ->
         str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")"
 
-  let pr_opt_type pr = function
-    | CHole (_,_,Misctypes.IntroAnonymous,_) -> mt ()
-    | t -> cut () ++ str ":" ++ pr t
-
   let pr_opt_type_spc pr = function
     | CHole (_,_,Misctypes.IntroAnonymous,_) -> mt ()
     | t ->  str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index e4a87739b1..58475630e6 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -395,10 +395,6 @@ open Decl_kinds
          pr_opt (pr_guard_annot pr_lconstr_expr bl) guard ++
          str":" ++ pr_spc_lconstr c)
 
-  let pr_priority = function
-    | None -> mt ()
-    | Some i -> spc () ++ str "|" ++ spc () ++ int i
-
 (**************************************)
 (* Pretty printer for vernac commands *)
 (**************************************)
diff --git a/printing/printer.ml b/printing/printer.ml
index 35ddf2e8cf..93d221f03f 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -370,11 +370,6 @@ let pr_context_limit_compact ?n env sigma =
       env ~init:(mt ()) in
   (sign_env ++ db_env)
 
-(* compact printing an env (variables and de Bruijn). Separator: three
-   spaces between simple hyps, and newline otherwise *)
-let pr_context_unlimited_compact env sigma =
-  pr_context_limit_compact env sigma
-
 (* The number of printed hypothesis in a goal *)
 (* If [None], no limit *)
 let print_hyps_limit = ref (None : int option)
-- 
cgit v1.2.3


From 4e84e83911c1cf7613a35b921b1e68e097f84b5a Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:11:47 +0200
Subject: Remove unused [open] statements

---
 printing/prettyp.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'printing')

diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 38e1110344..6841781ccd 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -8,7 +8,6 @@
 
 open Pp
 open Names
-open Term
 open Environ
 open Reductionops
 open Libnames
-- 
cgit v1.2.3


From 87910d7be9bd50de4db80f70c6e287c7c7994460 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Tue, 25 Apr 2017 14:31:15 +0200
Subject: Fix 4.04 warnings

---
 printing/prettyp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'printing')

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index aa422e36af..381af83c73 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -29,7 +29,7 @@ open Printer
 open Printmod
 open Context.Rel.Declaration
 
-module RelDecl = Context.Rel.Declaration
+(* module RelDecl = Context.Rel.Declaration *)
 module NamedDecl = Context.Named.Declaration
 
 type object_pr = {
-- 
cgit v1.2.3


From e9b745af47ba3386724b874e3fd74b6dad33b015 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Thu, 6 Apr 2017 22:48:32 +0200
Subject: Allow flexible anonymous universes in instances and sorts.

The addition to the test suite showcases the usage.
---
 printing/ppconstr.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'printing')

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 3041ac259e..b546c39aec 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -151,8 +151,8 @@ let tag_var = tag Tag.variable
 
   let pr_univ l =
     match l with
-      | [_,x] -> str x
-      | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> str (snd x)) l ++ str")"
+      | [_,x] -> pr_name x
+      | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> pr_name (snd x)) l ++ str")"
 
   let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}"
 
@@ -166,7 +166,7 @@ let tag_var = tag Tag.variable
     | GProp -> tag_type (str "Prop")
     | GSet -> tag_type (str "Set")
     | GType None -> tag_type (str "Type")
-    | GType (Some (_, u)) -> tag_type (str u)
+    | GType (Some (_, u)) -> tag_type (pr_name u)
 
   let pr_qualid sp =
     let (sl, id) = repr_qualid sp in
@@ -191,7 +191,7 @@ let tag_var = tag Tag.variable
       tag_type (str "Set")
     | GType u ->
       (match u with
-        | Some (_,u) -> str u
+        | Some (_,u) -> pr_name u
         | None -> tag_type (str "Type"))
 
   let pr_universe_instance l =
-- 
cgit v1.2.3


From 952e9aea47d3fad2d0f488d968ff0e90fa403ebc Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Wed, 3 May 2017 11:37:08 +0200
Subject: Adding an even more compact mode for goal display.

We want to print variables in vertical boxes as much as possible.

The criterion to distinguish "variable" from "hypothesis" is not
obvious. We chose this one but may change it in the future:

X:T is a variable if T is not of type Prop AND T is "simple" which
means T is either id or (t T1 .. Tn) Ti's are sort-typed (typicall
Ti:Type, but not Ti:nat).
---
 printing/printer.ml  | 60 ++++++++++++++++++++++++++++++++++++++++++++++------
 printing/printer.mli |  5 ++++-
 2 files changed, 57 insertions(+), 8 deletions(-)

(limited to 'printing')

diff --git a/printing/printer.ml b/printing/printer.ml
index 93d221f03f..0e31a4a042 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -262,6 +262,13 @@ let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t*)
 (**********************************************************************)
 (* Contexts and declarations                                          *)
 
+
+(* Flag for compact display of goals *)
+
+let get_compact_context,set_compact_context =
+  let compact_context = ref false in
+  (fun () -> !compact_context),(fun b  -> compact_context := b)
+
 let pr_compacted_decl env sigma decl =
   let ids, pbody, typ = match decl with
     | CompactedDecl.LocalAssum (ids, typ) ->
@@ -342,15 +349,55 @@ let pr_ne_context_of header env sigma =
     List.is_empty (Environ.named_context env)  then (mt ())
   else let penv = pr_context_unlimited env sigma in (header ++ penv ++ fnl ())
 
+(* Heuristic for horizontalizing hypothesis:
+   Detecting variable which type is a simple id or of the form (t x y ...)
+   where t is a product or only sorts (typically [Type -> Type -> ...]
+   and not [nat -> nat -> ...] ).
+   + Special case for non-Prop dependent terms. *)
+let rec should_compact env sigma typ =
+  get_compact_context() &&
+    match kind_of_term typ with
+    | Rel _ | Var _ | Sort _ | Const _ | Ind _ -> true
+    | App (c,args) ->
+       let _,type_of_c = Typing.type_of env sigma c in
+       let _,type_of_typ = Typing.type_of env sigma typ in
+       not (is_Prop type_of_typ)
+       && (* These two more tests detect rare cases of non-Prop-sorted
+             dependent hypothesis:  *)
+       let lnamedtyp , _ = decompose_prod type_of_c in
+       (* c has a non dependent type *)
+       List.for_all (fun (_,typarg) -> isSort typarg) lnamedtyp
+       && (* and real arguments are recursively elligible to compaction. *)
+       Array.for_all (should_compact env sigma) args
+    | _ -> false
+
+
+(* If option Compact Contexts is set, we pack "simple" hypothesis in a
+   hov box (with three sapaces as a separator), the global box being a
+   v box *)
 let rec bld_sign_env env sigma ctxt pps =
   match ctxt with
   | [] -> pps
+  | CompactedDecl.LocalAssum (ids,typ)::ctxt' when should_compact env sigma typ ->
+    let pps',ctxt' = bld_sign_env_id env sigma ctxt (mt ()) true in
+    (* putting simple hyps in a more horizontal flavor *)
+    bld_sign_env env sigma ctxt' (pps ++ brk (0,0) ++ hov 0 pps')
   | d:: ctxt' ->
-     let pidt = pr_var_list_decl env sigma d in
-     let pps' = pps ++ brk (0,0) ++ pidt in
-     bld_sign_env env sigma ctxt' pps'
+    let pidt = pr_var_list_decl env sigma d in
+    let pps' = pps ++ brk (0,0) ++ pidt in
+    bld_sign_env env sigma ctxt' pps'
+and bld_sign_env_id env sigma ctxt pps is_start =
+  match ctxt with
+  | [] -> pps,ctxt
+  | CompactedDecl.LocalAssum(ids,typ) as d :: ctxt' when should_compact env sigma typ ->
+    let pidt = pr_var_list_decl env sigma d in
+    let pps' = pps ++ (if not is_start then brk (3,0) else (mt ())) ++ pidt in
+    bld_sign_env_id env sigma ctxt' pps' false
+  | _ -> pps,ctxt
 
 
+(* compact printing an env (variables and de Bruijn). Separator: three
+   spaces between simple hyps, and newline otherwise *)
 let pr_context_limit_compact ?n env sigma =
   let ctxt = Termops.compact_named_context (named_context env) in
   let lgth = List.length ctxt in
@@ -360,15 +407,14 @@ let pr_context_limit_compact ?n env sigma =
     | Some n when n > lgth -> lgth
     | Some n -> n in
   let ctxt_chopped,ctxt_hidden = Util.List.chop n_capped ctxt in
-  (* a dot line hinting the number of hiden hyps. *)
+  (* a dot line hinting the number of hidden hyps. *)
   let hidden_dots = String.make (List.length ctxt_hidden) '.' in
   let sign_env = v 0 (str hidden_dots ++ (mt ())
                  ++ bld_sign_env env sigma (List.rev ctxt_chopped) (mt ())) in
   let db_env =
-    fold_rel_context
-      (fun env d pps -> pps ++ fnl () ++ pr_rel_decl env sigma d)
+    fold_rel_context (fun env d pps -> pps ++ fnl () ++ pr_rel_decl env sigma d)
       env ~init:(mt ()) in
-  (sign_env ++ db_env)
+  sign_env ++ db_env
 
 (* The number of printed hypothesis in a goal *)
 (* If [None], no limit *)
diff --git a/printing/printer.mli b/printing/printer.mli
index 504392e35f..9c9f6e766a 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -111,6 +111,9 @@ val pr_pconstructor        : env -> pconstructor -> std_ppcmds
 
 
 (** Contexts *)
+(** Display compact contexts of goals (simple hyps on the same line) *)
+val set_compact_context : bool -> unit
+val get_compact_context : unit -> bool
 
 val pr_context_unlimited   : env -> evar_map -> std_ppcmds
 val pr_ne_context_of       : std_ppcmds -> env -> evar_map -> std_ppcmds
@@ -132,7 +135,7 @@ val pr_cpred               : Cpred.t -> std_ppcmds
 val pr_idpred              : Id.Pred.t -> std_ppcmds
 val pr_transparent_state   : transparent_state -> std_ppcmds
 
-(** Proofs *)
+(** Proofs, these functions obey [Hyps Limit] and [Compact contexts]. *)
 
 val pr_goal                : goal sigma -> std_ppcmds
 val pr_subgoals            : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds
-- 
cgit v1.2.3


From 1fe73e6af81759fa8b78c8660745492ed886d477 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Wed, 26 Apr 2017 11:57:58 +0200
Subject: Adding an option "Printing Unfocused".

Off by default.

+ small refactoring of emacs hacks in printer.ml.
---
 printing/printer.ml  | 139 ++++++++++++++++++++++++++++++++++-----------------
 printing/printer.mli |  21 +++++++-
 2 files changed, 111 insertions(+), 49 deletions(-)

(limited to 'printing')

diff --git a/printing/printer.ml b/printing/printer.ml
index 93d221f03f..3d67e89f51 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -34,6 +34,49 @@ let delayed_emacs_cmd s =
 let get_current_context () =
   Pfedit.get_current_context ()
 
+let enable_unfocused_goal_printing = ref false
+let enable_goal_tags_printing = ref false
+let enable_goal_names_printing = ref false
+
+let should_tag() = !enable_goal_tags_printing
+let should_unfoc() = !enable_unfocused_goal_printing
+let should_gname() = !enable_goal_names_printing
+
+
+let _ =
+  let open Goptions in
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "printing of unfocused goal";
+      optkey   = ["Printing";"Unfocused"];
+      optread  = (fun () -> !enable_unfocused_goal_printing);
+      optwrite = (fun b -> enable_unfocused_goal_printing:=b) }
+
+(* This is set on by proofgeneral proof-tree mode. But may be used for
+   other purposes *)
+let _ =
+  let open Goptions in
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "printing of goal tags";
+      optkey   = ["Printing";"Goal";"Tags"];
+      optread  = (fun () -> !enable_goal_tags_printing);
+      optwrite = (fun b -> enable_goal_tags_printing:=b) }
+
+
+let _ =
+  let open Goptions in
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "printing of goal names";
+      optkey   = ["Printing";"Goal";"Names"];
+      optread  = (fun () -> !enable_goal_names_printing);
+      optwrite = (fun b -> enable_goal_names_printing:=b) }
+
+
 (**********************************************************************)
 (** Terms                                                             *)
 
@@ -419,23 +462,25 @@ let default_pr_goal gs =
 (* display a goal tag *)
 let pr_goal_tag g =
   let s = " (ID " ^ Goal.uid g ^ ")" in
-  str (emacs_str s)
-
-let display_name = false
+  str s
 
 (* display a goal name *)
 let pr_goal_name sigma g =
-  if display_name then str " " ++ Pp.surround (pr_existential_key sigma g)
+  if should_gname() then str " " ++ Pp.surround (pr_existential_key sigma g)
   else mt ()
 
+let pr_goal_header nme sigma g =
+  let (g,sigma) = Goal.V82.nf_evar sigma g in
+  str "subgoal " ++ nme ++ (if should_tag() then pr_goal_tag g else str"")
+  ++ (if should_gname() then str " " ++ Pp.surround (pr_existential_key sigma g) else mt ())  
+
 (* display the conclusion of a goal *)
 let pr_concl n sigma g =
   let (g,sigma) = Goal.V82.nf_evar sigma g in
   let env = Goal.V82.env sigma g in
   let pc = pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) in
-    str (emacs_str "")  ++
-      str "subgoal " ++ int n ++ pr_goal_tag g ++ pr_goal_name sigma g ++
-      str " is:" ++ cut () ++ str" "  ++ pc
+  let header = pr_goal_header (int n) sigma g in
+  header ++ str " is:" ++ cut () ++ str" "  ++ pc
 
 (* display evar type: a context and a type *)
 let pr_evgl_sign sigma evi =
@@ -491,8 +536,8 @@ let pr_ne_evar_set hd tl sigma l =
 
 let pr_selected_subgoal name sigma g =
   let pg = default_pr_goal { sigma=sigma ; it=g; } in
-  v 0 (str "subgoal " ++ name ++ pr_goal_tag g ++ pr_goal_name sigma g
-       ++ str " is:" ++ cut () ++ pg)
+  let header = pr_goal_header name sigma g in
+  v 0 (header ++ str " is:" ++ cut () ++ pg)
 
 let default_pr_subgoal n sigma =
   let rec prrec p = function
@@ -585,27 +630,27 @@ let print_dependent_evars gl sigma seeds =
 	      end i (str ",")
 	end evars (str "")
     in
-    fnl () ++
-    str "(dependent evars:" ++ evars ++ str ")" ++ fnl ()
-    else
-      fnl () ++
-	str "(dependent evars: (printing disabled) )" ++ fnl ()
+    cut () ++ cut () ++
+    str "(dependent evars:" ++ evars ++ str ")"
+    else if !Flags.print_emacs then
+      (* IDEs prefer something dummy instead of nothing *)
+      cut () ++ cut () ++ str "(dependent evars: (printing disabled) )"
+    else mt ()
   in
-  constraints ++ delayed_emacs_cmd evars
+  constraints ++ evars ()
 
 (* Print open subgoals. Checks for uninstantiated existential variables *)
 (* spiwack: [seeds] is for printing dependent evars in emacs mode. *)
 (* spiwack: [pr_first] is true when the first goal must be singled out
    and printed in its entirety. *)
-(* courtieu: in emacs mode, even less cases where the first goal is printed
-   in its entirety *)
-let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals =
+let default_pr_subgoals ?(pr_first=true)
+                        close_cmd sigma seeds shelf stack unfocused goals =
   (** Printing functions for the extra informations. *)
   let rec print_stack a = function
     | [] -> Pp.int a
     | b::l -> Pp.int a ++ str"-" ++ print_stack b l
   in
-  let print_unfocused l =
+  let print_unfocused_nums l =
     match l with
     | [] -> None
     | a::l -> Some (str"unfocused: " ++ print_stack a l)
@@ -625,7 +670,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals
     | [] -> Pp.mt ()
     | a::l -> Pp.spc () ++ str"(" ++ print_comma_separated_list a l ++ str")"
   in
-  let extra = Option.List.flatten [ print_unfocused stack ; print_shelf shelf ] in
+  let extra = Option.List.flatten [ print_unfocused_nums stack ; print_shelf shelf ] in
   let print_extra = print_extra_list extra in
   let focused_if_needed =
     let needed = not (CList.is_empty extra) && pr_first in
@@ -642,8 +687,9 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals
   in
   let print_multiple_goals g l =
     if pr_first then
-      default_pr_goal { it = g ; sigma = sigma; } ++ fnl () ++
-      pr_rec 2 l
+      default_pr_goal { it = g ; sigma = sigma; }
+      ++ (if l=[] then str"" else cut ())
+      ++ pr_rec 2 l
     else 
       pr_rec 1 (g::l)
   in
@@ -658,32 +704,27 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals
       begin
 	let exl = Evarutil.non_instantiated sigma in
 	if Evar.Map.is_empty exl then
-	  (str"No more subgoals."
-	   ++ print_dependent_evars None sigma seeds)
+	  (str"No more subgoals." ++ print_dependent_evars None sigma seeds)
 	else
 	  let pei = pr_evars_int sigma 1 exl in
-	  (str "No more subgoals, but there are non-instantiated existential variables:"
-	   ++ fnl () ++ (hov 0 pei)
-	   ++ print_dependent_evars None sigma seeds ++ fnl () ++
-           str "You can use Grab Existential Variables.")
+	  v 0 ((str "No more subgoals,"
+                ++ str " but there are non-instantiated existential variables:"
+	        ++ cut () ++ (hov 0 pei)
+                ++ print_dependent_evars None sigma seeds
+                ++ cut () ++ str "You can use Grab Existential Variables."))
       end
-  | [g] when not !Flags.print_emacs && pr_first ->
-      let pg = default_pr_goal { it = g ; sigma = sigma; } in
-      v 0 (
-	str "1" ++ focused_if_needed ++ str"subgoal" ++ print_extra
-        ++ pr_goal_tag g ++ pr_goal_name sigma g ++ cut () ++ pg
-	++ print_dependent_evars (Some g) sigma seeds
-      )
   | g1::rest ->
       let goals = print_multiple_goals g1 rest in
       let ngoals = List.length rest+1 in
       v 0 (
-	int ngoals ++ focused_if_needed ++ str(String.plural ngoals "subgoal") ++
-          print_extra ++
-          str ((if display_name then (fun x -> x) else emacs_str) ", subgoal 1")
-        ++ pr_goal_tag g1
-        ++ pr_goal_name sigma g1 ++ cut ()
-	++ goals
+	int ngoals ++ focused_if_needed ++ str(String.plural ngoals "subgoal")
+        ++ print_extra
+        ++ str (if (should_gname()) then ", subgoal 1" else "")
+        ++ (if should_tag() then pr_goal_tag g1 else str"")
+        ++ pr_goal_name sigma g1 ++ cut () ++ goals
+        ++ (if unfocused=[] then str ""
+           else (cut() ++ cut() ++ str "*** Unfocused goals:" ++ cut()
+                 ++ pr_rec (List.length rest + 2) unfocused))
 	++ print_dependent_evars (Some g1) sigma seeds
       )
 
@@ -692,7 +733,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals
 
 
 type printer_pr = {
- pr_subgoals            : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds;
+ pr_subgoals            : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> std_ppcmds;
  pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds;
  pr_goal                : goal sigma -> std_ppcmds;
 }
@@ -726,16 +767,16 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
   begin match goals with
   | [] -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in
           begin match bgoals,shelf,given_up with
-	  | [] , [] , [] -> pr_subgoals None sigma seeds shelf stack goals
+	  | [] , [] , [] -> pr_subgoals None sigma seeds shelf stack [] goals
           | [] , [] , _ ->
 	     Feedback.msg_info (str "No more subgoals, but there are some goals you gave up:");
 	     fnl ()
-            ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] given_up
+            ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] [] given_up
             ++ fnl () ++ str "You need to go back and solve them."
           | [] , _ , _ ->
 	    Feedback.msg_info (str "All the remaining goals are on the shelf.");
 	    fnl ()
-            ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] shelf
+            ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] [] shelf
 	  | _ , _, _ ->
             let end_cmd =
               str "This subproof is complete, but there are some unfocused goals." ++
@@ -743,9 +784,13 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
                if Pp.ismt s then s else fnl () ++ s) ++
               fnl ()
             in
-	    pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] bgoals
+	    pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] [] bgoals
 	  end
-  | _ -> pr_subgoals None sigma seeds shelf stack goals
+  | _ -> 
+     let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in
+     let bgoals_focused, bgoals_unfocused = List.partition (fun x -> List.mem x goals) bgoals in
+     let unfocused_if_needed = if should_unfoc() then bgoals_unfocused else [] in
+     pr_subgoals ~pr_first:true None bsigma seeds shelf [] unfocused_if_needed bgoals_focused
   end
 
 let pr_nth_open_subgoal n =
diff --git a/printing/printer.mli b/printing/printer.mli
index 504392e35f..c282950545 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -18,6 +18,11 @@ open Glob_term
 
 (** These are the entry points for printing terms, context, tac, ... *)
 
+
+val enable_unfocused_goal_printing: bool ref
+val enable_goal_tags_printing      : bool ref
+val enable_goal_names_printing     : bool ref
+
 (** Terms *)
 
 val pr_lconstr_env         : env -> evar_map -> constr -> std_ppcmds
@@ -135,7 +140,19 @@ val pr_transparent_state   : transparent_state -> std_ppcmds
 (** Proofs *)
 
 val pr_goal                : goal sigma -> std_ppcmds
-val pr_subgoals            : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds
+
+(** [pr_subgoals ~pr_first pp sigma seeds shelf focus_stack unfocused goals]
+   prints the goals of the list [goals] followed by the goals in
+   [unfocused], in a short way (typically only the conclusion) except
+   for the first goal if [pr_first] is true. This function can be
+   replaced by another one by calling [set_printer_pr] (see below),
+   typically by plugin writers. The default printer prints only the
+   focused goals unless the conrresponding option
+   [enable_unfocused_goal_printing] is set. [seeds] is for printing
+   dependent evars (mainly for emacs proof tree mode). *)
+val pr_subgoals            : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list
+                             -> goal list -> goal list -> std_ppcmds
+
 val pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds
 val pr_concl               : int -> evar_map -> goal -> std_ppcmds
 
@@ -190,7 +207,7 @@ val pr_goal_by_id : Id.t -> std_ppcmds
 val pr_goal_by_uid : string -> std_ppcmds
 
 type printer_pr = {
- pr_subgoals            : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds;
+ pr_subgoals            : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> std_ppcmds;
  pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds;
  pr_goal                : goal sigma -> std_ppcmds;
 };;
-- 
cgit v1.2.3


From 8bcf71360261d789ac3ab919bc49309df678628f Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Tue, 2 May 2017 21:32:26 +0200
Subject: labelizing arguments

---
 printing/printer.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'printing')

diff --git a/printing/printer.ml b/printing/printer.ml
index 3d67e89f51..1d3e67d9d6 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -688,7 +688,7 @@ let default_pr_subgoals ?(pr_first=true)
   let print_multiple_goals g l =
     if pr_first then
       default_pr_goal { it = g ; sigma = sigma; }
-      ++ (if l=[] then str"" else cut ())
+      ++ (if l=[] then mt () else cut ())
       ++ pr_rec 2 l
     else 
       pr_rec 1 (g::l)
-- 
cgit v1.2.3


From 8bdb00bbea9dce95f7e0bc18250a41545660299d Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Thu, 4 May 2017 11:25:22 +0200
Subject: Warning removed.

---
 printing/printer.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'printing')

diff --git a/printing/printer.ml b/printing/printer.ml
index 1d3e67d9d6..91a7d22899 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -28,8 +28,6 @@ module CompactedDecl = Context.Compacted.Declaration
 
 let emacs_str s =
   if !Flags.print_emacs then s else ""
-let delayed_emacs_cmd s =
-  if !Flags.print_emacs then s () else str ""
 
 let get_current_context () =
   Pfedit.get_current_context ()
-- 
cgit v1.2.3


From 91d78c590b35c9edcf9f68c408ba82090f68e156 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Fri, 5 May 2017 12:59:41 +0200
Subject: Adapted to EConstr.

---
 printing/printer.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'printing')

diff --git a/printing/printer.ml b/printing/printer.ml
index 0e31a4a042..997d866f92 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -359,14 +359,14 @@ let rec should_compact env sigma typ =
     match kind_of_term typ with
     | Rel _ | Var _ | Sort _ | Const _ | Ind _ -> true
     | App (c,args) ->
-       let _,type_of_c = Typing.type_of env sigma c in
-       let _,type_of_typ = Typing.type_of env sigma typ in
-       not (is_Prop type_of_typ)
+       let _,type_of_c = Typing.type_of env sigma (EConstr.of_constr c) in
+       let _,type_of_typ = Typing.type_of env sigma (EConstr.of_constr typ) in
+       not (is_Prop (EConstr.to_constr sigma type_of_typ))
        && (* These two more tests detect rare cases of non-Prop-sorted
              dependent hypothesis:  *)
-       let lnamedtyp , _ = decompose_prod type_of_c in
+       let lnamedtyp , _ = EConstr.decompose_prod sigma type_of_c in
        (* c has a non dependent type *)
-       List.for_all (fun (_,typarg) -> isSort typarg) lnamedtyp
+       List.for_all (fun (_,typarg) -> EConstr.isSort sigma typarg) lnamedtyp
        && (* and real arguments are recursively elligible to compaction. *)
        Array.for_all (should_compact env sigma) args
     | _ -> false
@@ -389,7 +389,7 @@ let rec bld_sign_env env sigma ctxt pps =
 and bld_sign_env_id env sigma ctxt pps is_start =
   match ctxt with
   | [] -> pps,ctxt
-  | CompactedDecl.LocalAssum(ids,typ) as d :: ctxt' when should_compact env sigma typ ->
+ | CompactedDecl.LocalAssum(ids,typ) as d :: ctxt' when should_compact env sigma typ ->
     let pidt = pr_var_list_decl env sigma d in
     let pps' = pps ++ (if not is_start then brk (3,0) else (mt ())) ++ pidt in
     bld_sign_env_id env sigma ctxt' pps' false
-- 
cgit v1.2.3


From 697cd5a8e7927873ed6700c7e906ae3675bd98b1 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Fri, 12 May 2017 10:30:50 +0200
Subject: Simplified compaction criterion + tests.

---
 printing/printer.ml | 25 +++++--------------------
 1 file changed, 5 insertions(+), 20 deletions(-)

(limited to 'printing')

diff --git a/printing/printer.ml b/printing/printer.ml
index 997d866f92..3feea65964 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -349,27 +349,12 @@ let pr_ne_context_of header env sigma =
     List.is_empty (Environ.named_context env)  then (mt ())
   else let penv = pr_context_unlimited env sigma in (header ++ penv ++ fnl ())
 
-(* Heuristic for horizontalizing hypothesis:
-   Detecting variable which type is a simple id or of the form (t x y ...)
-   where t is a product or only sorts (typically [Type -> Type -> ...]
-   and not [nat -> nat -> ...] ).
-   + Special case for non-Prop dependent terms. *)
-let rec should_compact env sigma typ =
+(* Heuristic for horizontalizing hypothesis that the user probably
+   considers as "variables": An hypothesis H:T where T:S and S<>Prop. *)
+let should_compact env sigma typ =
   get_compact_context() &&
-    match kind_of_term typ with
-    | Rel _ | Var _ | Sort _ | Const _ | Ind _ -> true
-    | App (c,args) ->
-       let _,type_of_c = Typing.type_of env sigma (EConstr.of_constr c) in
-       let _,type_of_typ = Typing.type_of env sigma (EConstr.of_constr typ) in
-       not (is_Prop (EConstr.to_constr sigma type_of_typ))
-       && (* These two more tests detect rare cases of non-Prop-sorted
-             dependent hypothesis:  *)
-       let lnamedtyp , _ = EConstr.decompose_prod sigma type_of_c in
-       (* c has a non dependent type *)
-       List.for_all (fun (_,typarg) -> EConstr.isSort sigma typarg) lnamedtyp
-       && (* and real arguments are recursively elligible to compaction. *)
-       Array.for_all (should_compact env sigma) args
-    | _ -> false
+    let type_of_typ = Retyping.get_type_of env sigma (EConstr.of_constr typ) in
+    not (is_Prop (EConstr.to_constr sigma type_of_typ))
 
 
 (* If option Compact Contexts is set, we pack "simple" hypothesis in a
-- 
cgit v1.2.3


From c1e9a27d383688e44ba34ada24fe08151cb5846e Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 17 May 2017 21:04:18 +0200
Subject: [vernac] Remove `Save thm id.` command.

We'd like to cleanup the `proof_end` type so we can have a smaller
path in proof save. Note that the construction:

```
Goal Type.
⋮
Save id.
```

has to be handled by the STM in the same path as Defined (but with an
opaque flag), as `Save id` will alter the environment and cannot be
processed in parallel.

We thus try to simply such paths a bit, as complexity of `lemmas.ml`
seems like an issue these days. The form `Save Theorem id` doesn't
really seem used, and moreover we should really add a type of "Goal",
and unify syntax.

It is often the case that beginners try `Goal addnC n : n + 0 = n."
etc...
---
 printing/ppvernac.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 3e41439c8c..76f1d8dd71 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -721,9 +721,7 @@ open Decl_kinds
               | Opaque (Some l) ->
                   keyword "Qed" ++ spc() ++ str"export" ++
                     prlist_with_sep (fun () -> str", ") pr_lident l)
-          | Some (id,th) -> (match th with
-              | None -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id
-              | Some tok -> keyword "Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_lident id)
+          | Some id -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id
       )
       | VernacExactProof c ->
         return (hov 2 (keyword "Proof" ++ pr_lconstrarg c))
-- 
cgit v1.2.3