Imported Upstream version 8.5~beta3+dfsg

10 files changed, 236 insertions, 315 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index d9d8af66..ea705e33 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -140,8 +140,8 @@ end) = struct
 
   let pr_univ l =
     match l with
-      | [x] -> str x
-      | l -> str"max(" ++ prlist_with_sep (fun () -> str",") str l ++ str")"
+      | [_,x] -> str x
+      | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> str (snd x)) l ++ str")"
 
   let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}"
 
@@ -174,7 +174,7 @@ end) = struct
       tag_type (str "Set")
     | GType u ->
       (match u with
-        | Some u -> str u
+        | Some (_,u) -> str u
         | None -> tag_type (str "Type"))
 
   let pr_universe_instance l =
@@ -676,11 +676,11 @@ end) = struct
         return (pr_glob_sort s, latom)
       | CCast (_,a,b) ->
         return (
-          hv 0 (pr mt (lcast,L) a ++ cut () ++
+          hv 0 (pr mt (lcast,L) a ++ spc () ++
                   match b with
-                    | CastConv b -> str ":" ++ pr mt (-lcast,E) b
-                    | CastVM b -> str "<:" ++ pr mt (-lcast,E) b
-                    | CastNative b -> str "<<:" ++ pr mt (-lcast,E) b
+                    | CastConv b -> str ":" ++ ws 1 ++ pr mt (-lcast,E) b
+                    | CastVM b -> str "<:" ++ ws 1 ++ pr mt (-lcast,E) b
+                    | CastNative b -> str "<<:" ++ ws 1 ++ pr mt (-lcast,E) b
                     | CastCoerce -> str ":>"),
           lcast
         )
diff --git a/printing/ppstyle.ml b/printing/ppstyle.ml
deleted file mode 100644
index fb334c70..00000000
--- a/printing/ppstyle.ml
+++ /dev/null
@@ -1,149 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Util
-
-type t = string
-(** We use the concatenated string, with dots separating each string. We
-    forbid the use of dots in the strings. *)
-
-let tags : Terminal.style option String.Map.t ref = ref String.Map.empty
-
-let make ?style tag =
-  let check s = if String.contains s '.' then invalid_arg "Ppstyle.make" in
-  let () = List.iter check tag in
-  let name = String.concat "." tag in
-  let () = assert (not (String.Map.mem name !tags)) in
-  let () = tags := String.Map.add name style !tags in
-  name
-
-let repr t = String.split '.' t
-
-let get_style tag =
-  try String.Map.find tag !tags with Not_found -> assert false
-
-let set_style tag st =
-  try tags := String.Map.update tag st !tags with Not_found -> assert false
-
-let clear_styles () =
-  tags := String.Map.map (fun _ -> None) !tags
-
-let dump () = String.Map.bindings !tags
-
-let parse_config s =
-  let styles = Terminal.parse s in
-  let set accu (name, st) =
-    try String.Map.update name (Some st) accu with Not_found -> accu
-  in
-  tags := List.fold_left set !tags styles
-
-let tag = Pp.Tag.create "ppstyle"
-
-(** Default tag is to reset everything *)
-let default = Terminal.({
-  fg_color = Some `DEFAULT;
-  bg_color = Some `DEFAULT;
-  bold = Some false;
-  italic = Some false;
-  underline = Some false;
-  negative = Some false;
-})
-
-let empty = Terminal.make ()
-
-let make_style_stack style_tags =
-  (** Not thread-safe. We should put a lock somewhere if we print from
-      different threads. Do we? *)
-  let style_stack = ref [] in
-  let peek () = match !style_stack with
-  | [] -> default (** Anomalous case, but for robustness *)
-  | st :: _ -> st
-  in
-  let push tag =
-    let style =
-      try
-        begin match String.Map.find tag style_tags with
-        | None -> empty
-        | Some st -> st
-        end
-      with Not_found -> empty
-    in
-    (** Use the merging of the latest tag and the one being currently pushed.
-    This may be useful if for instance the latest tag changes the background and
-    the current one the foreground, so that the two effects are additioned. *)
-    let style = Terminal.merge (peek ()) style in
-    let () = style_stack := style :: !style_stack in
-    Terminal.eval style
-  in
-  let pop _ = match !style_stack with
-  | [] ->
-    (** Something went wrong, we fallback *)
-    Terminal.eval default
-  | _ :: rem ->
-    let () = style_stack := rem in
-    Terminal.eval (peek ())
-  in
-  let clear () = style_stack := [] in
-  push, pop, clear
-
-let error_tag =
-  let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`RED () in
-  make ~style ["message"; "error"]
-
-let warning_tag =
-  let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`YELLOW () in
-  make ~style ["message"; "warning"]
-
-let debug_tag =
-  let style = Terminal.make ~bold:true ~fg_color:`WHITE ~bg_color:`MAGENTA () in
-  make ~style ["message"; "debug"]
-
-let pp_tag t = match Pp.Tag.prj t tag with
-| None -> ""
-| Some key -> key
-
-let init_color_output () =
-  let push_tag, pop_tag, clear_tag = make_style_stack !tags in
-  let tag_handler = {
-    Format.mark_open_tag = push_tag;
-    Format.mark_close_tag = pop_tag;
-    Format.print_open_tag = ignore;
-    Format.print_close_tag = ignore;
-  } in
-  let open Pp_control in
-  let () = Format.pp_set_mark_tags !std_ft true in
-  let () = Format.pp_set_mark_tags !err_ft true in
-  let () = Format.pp_set_formatter_tag_functions !std_ft tag_handler in
-  let () = Format.pp_set_formatter_tag_functions !err_ft tag_handler in
-  let pptag = tag in
-  let open Pp in
-  let msg ?header ft strm =
-    let strm = match header with
-    | None -> hov 0 strm
-    | Some (h, t) ->
-      let tag = Pp.Tag.inj t pptag in
-      let h = Pp.tag tag (str h ++ str ":") in
-      hov 0 (h ++ spc () ++ strm)
-    in
-    pp_with ~pp_tag ft strm;
-    Format.pp_print_newline ft ();
-    Format.pp_print_flush ft ();
-    (** In case something went wrong, we reset the stack *)
-    clear_tag ();
-  in
-  let logger level strm = match level with
-  | Debug _ -> msg ~header:("Debug", debug_tag) !std_ft strm
-  | Info -> msg !std_ft strm
-  | Notice -> msg !std_ft strm
-  | Warning ->
-    let header = ("Warning", warning_tag) in
-    Flags.if_warn (fun () -> msg ~header !err_ft strm) ()
-  | Error -> msg ~header:("Error", error_tag) !err_ft strm
-  in
-  let () = set_logger logger in
-  ()
diff --git a/printing/ppstyle.mli b/printing/ppstyle.mli
deleted file mode 100644
index f5d6184c..00000000
--- a/printing/ppstyle.mli
+++ /dev/null
@@ -1,70 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** Highlighting of printers. Used for pretty-printing terms that should be
-    displayed on a color-capable terminal. *)
-
-(** {5 Style tags} *)
-
-type t
-(** Style tags *)
-
-val make : ?style:Terminal.style -> string list -> t
-(** Create a new tag with the given name. Each name must be unique. The optional
-    style is taken as the default one. *)
-
-val repr : t -> string list
-(** Gives back the original name of the style tag where each string has been
-    concatenated and separated with a dot. *)
-
-val tag : t Pp.Tag.key
-(** An annotation for styles *)
-
-(** {5 Manipulating global styles} *)
-
-val get_style : t -> Terminal.style option
-(** Get the style associated to a tag. *)
-
-val set_style : t -> Terminal.style option -> unit
-(** Set a style associated to a tag. *)
-
-val clear_styles : unit -> unit
-(** Clear all styles. *)
-
-val parse_config : string -> unit
-(** Add all styles from the given string as parsed by {!Terminal.parse}.
-    Unregistered tags are ignored. *)
-
-val dump : unit -> (t * Terminal.style option) list
-(** Recover the list of known tags together with their current style. *)
-
-(** {5 Setting color output} *)
-
-val init_color_output : unit -> unit
-(** Once called, all tags defined here will use their current style when
-    printed. To this end, this function redefines the loggers used when sending
-    messages to the user. The program will in particular use the formatters
-    {!Pp_control.std_ft} and {!Pp_control.err_ft} to display those messages,
-    with additional syle information provided by this module. Be careful this is
-    not compatible with the Emacs mode! *)
-
-val pp_tag : Pp.tag_handler
-(** Returns the name of a style tag that is understandable by the formatters
-    that have been inititialized through {!init_color_output}. To be used with
-    {!Pp.pp_with}. *)
-
-(** {5 Tags} *)
-
-val error_tag : t
-(** Tag used by the {!Pp.msg_error} function. *)
-
-val warning_tag : t
-(** Tag used by the {!Pp.msg_warning} function. *)
-
-val debug_tag : t
-(** Tag used by the {!Pp.msg_debug} function. *)
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index f8264e5a..a669aef9 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1260,13 +1260,12 @@ module Make
 
         and pr_tacarg = function
           | TacDynamic (loc,t) ->
-            pr_with_comments loc (
-              str "<" ++ keyword "dynamic" ++ str (" [" ^ (Dyn.tag t)^"]>")
-            )
+            pr_with_comments loc
+              (str "<" ++ keyword "dynamic" ++ str " [" ++ str (Dyn.tag t) ++ str "]>")
           | MetaIdArg (loc,true,s) ->
-            pr_with_comments loc (str ("$" ^ s))
+            pr_with_comments loc (str "$" ++ str s)
           | MetaIdArg (loc,false,s) ->
-            pr_with_comments loc (keyword "constr:" ++ str(" $" ^ s))
+            pr_with_comments loc (keyword "constr:" ++ str " $" ++ str s)
           | Reference r ->
             pr.pr_reference r
           | ConstrMayEval c ->
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 89ffae4b..72b9cafe 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -43,6 +43,12 @@ module Make
     else
       pr_id id
 
+  let pr_plident (lid, l) =
+    pr_lident lid ++
+    (match l with
+     | Some l -> prlist_with_sep spc pr_lident l
+     | None -> mt())
+    
   let string_of_fqid fqid =
     String.concat "." (List.map Id.to_string fqid)
 
@@ -160,6 +166,8 @@ module Make
     (* This should not happen because of the grammar *)
       | IntValue (Some n) -> spc() ++ int n
       | StringValue s -> spc() ++ str s
+      | StringOptValue None -> mt()
+      | StringOptValue (Some s) -> spc() ++ str s
       | BoolValue b -> mt()
     in pr_printoption a None ++ pr_opt_value b
 
@@ -348,6 +356,7 @@ module Make
       | l ->
         prlist_with_sep spc
           (fun p -> hov 1 (str "(" ++ pr_params pr_c p ++ str ")")) l
+
 (*
   prlist_with_sep pr_semicolon (pr_params pr_c)
 *)
@@ -387,10 +396,16 @@ module Make
              hov 0 (prlist_with_sep sep pr_production_item pil ++
                       spc() ++ str":=" ++ spc() ++ pr_raw_tactic t))
 
-  let pr_statement head (id,(bl,c,guard)) =
-    assert (not (Option.is_empty id));
+  let pr_univs pl =
+    match pl with
+    | None -> mt ()
+    | Some pl -> str"@{" ++ prlist_with_sep spc pr_lident pl ++ str"}"
+
+  let pr_statement head (idpl,(bl,c,guard)) =
+    assert (not (Option.is_empty idpl));
+    let id, pl = Option.get idpl in
     hov 2
-      (head ++ spc() ++ pr_lident (Option.get id) ++ spc() ++
+      (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)
@@ -579,7 +594,8 @@ module Make
           let pr_goal_reference = function
             | OpenSubgoals -> mt ()
             | NthGoal n -> spc () ++ int n
-            | GoalId n -> spc () ++ str n in
+            | GoalId id -> spc () ++ pr_id id
+            | GoalUid n -> spc () ++ str n in
           let pr_showable = function
             | ShowGoal n -> keyword "Show" ++ pr_goal_reference n
             | ShowGoalImplicitly n -> keyword "Show Implicit Arguments" ++ pr_opt int n
@@ -627,6 +643,8 @@ module Make
           )
         | VernacTime v ->
           return (keyword "Time" ++ spc() ++ pr_vernac_list v)
+        | VernacRedirect (s, v) ->
+          return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_list v)
         | VernacTimeout(n,v) ->
           return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac v)
         | VernacFail v ->
@@ -642,11 +660,15 @@ module Make
             keyword (if opening then "Open " else "Close ") ++
               keyword "Scope" ++ spc() ++ str sc
           )
-        | VernacDelimiters (sc,key) ->
+        | VernacDelimiters (sc,Some key) ->
           return (
             keyword "Delimit Scope" ++ spc () ++ str sc ++
               spc() ++ keyword "with" ++ spc () ++ str key
           )
+        | VernacDelimiters (sc, None) ->
+          return (
+            keyword "Undelimit Scope" ++ spc () ++ str sc
+          )
         | VernacBindScope (sc,cll) ->
           return (
             keyword "Bind Scope" ++ spc () ++ str sc ++
@@ -723,7 +745,7 @@ module Make
           return (
             hov 2 (
               pr_def_token d ++ spc()
-              ++ pr_lident id ++ binds ++ typ
+              ++ pr_plident id ++ binds ++ typ
               ++ (match c with
                 | None -> mt()
                 | Some cc -> str" :=" ++ spc() ++ cc))
@@ -754,11 +776,12 @@ module Make
           return (hov 2 (keyword "Proof" ++ pr_lconstrarg c))
         | VernacAssumption (stre,_,l) ->
           let n = List.length (List.flatten (List.map fst (List.map snd l))) in
-          return (
-            hov 2
-              (pr_assumption_token (n > 1) stre ++ spc() ++
-                 pr_ne_params_list pr_lconstr_expr l)
-          )
+          let pr_params (c, (xl, t)) =
+            hov 2 (prlist_with_sep sep pr_plident xl ++ spc() ++
+              (if c then str":>" else str":" ++ spc() ++ pr_lconstr_expr t))
+          in
+          let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in
+          return (hov 2 (pr_assumption_token (n > 1) stre ++ spc() ++ assumptions))
         | VernacInductive (p,f,l) ->
           let pr_constructor (coe,(id,c)) =
             hov 2 (pr_lident id ++ str" " ++
@@ -775,10 +798,10 @@ module Make
             | RecordDecl (c,fs) ->
               pr_record_decl b c fs
           in
-          let pr_oneind key (((coe,id),indpar,s,k,lc),ntn) =
+          let pr_oneind key (((coe,(id,pl)),indpar,s,k,lc),ntn) =
             hov 0 (
               str key ++ spc() ++
-                (if coe then str"> " else str"") ++ pr_lident id ++
+                (if coe then str"> " else str"") ++ pr_lident id ++ pr_univs pl ++
                 pr_and_type_binders_arg indpar ++ spc() ++
                 Option.cata (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) (mt()) s ++
                 str" :=") ++ pr_constructor_list k lc ++
@@ -802,9 +825,9 @@ module Make
             | None | Some Global -> ""
           in
           let pr_onerec = function
-            | ((loc,id),ro,bl,type_,def),ntn ->
+            | (((loc,id),pl),ro,bl,type_,def),ntn ->
               let annot = pr_guard_annot pr_lconstr_expr bl ro in
-              pr_id id ++ pr_binders_arg bl ++ annot
+              pr_id id ++ pr_univs pl ++ pr_binders_arg bl ++ annot
               ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
               ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++
                 prlist (pr_decl_notation pr_constr) ntn
@@ -820,8 +843,8 @@ module Make
             | Some Local -> keyword "Local" ++ spc ()
             | None | Some Global -> str ""
           in
-          let pr_onecorec (((loc,id),bl,c,def),ntn) =
-            pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
+          let pr_onecorec ((((loc,id),pl),bl,c,def),ntn) =
+            pr_id id ++ pr_univs pl ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
               spc() ++ pr_lconstr_expr c ++
               pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++
               prlist (pr_decl_notation pr_constr) ntn
@@ -1253,7 +1276,7 @@ module Make
     and pr_extend s cl =
       let pr_arg a =
         try pr_gen a
-        with Failure _ -> str ("<error in "^fst s^">") in
+        with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in
       try
         let rl = Egramml.get_extend_vernac_rule s in
         let start,rl,cl =
@@ -1271,7 +1294,7 @@ module Make
             (start,cl) rl in
         hov 1 pp
       with Not_found ->
-        hov 1 (str ("TODO("^fst s) ++ prlist_with_sep sep pr_arg cl ++ str ")")
+        hov 1 (str "TODO(" ++ str (fst s) ++ prlist_with_sep sep pr_arg cl ++ str ")")
 
     in pr_vernac
 
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 4a66c33d..84649e6e 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -73,8 +73,15 @@ let print_ref reduce ref =
       in it_mkProd_or_LetIn ccl ctx
     else typ in
   let univs = Global.universes_of_global ref in
-  hov 0 (pr_global ref ++ str " :" ++ spc () ++ pr_ltype typ ++ 
-  	   Printer.pr_universe_ctx univs)
+  let env = Global.env () in
+  let bl = Universes.universe_binders_of_global ref in
+  let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
+  let inst =
+    if Global.is_polymorphic ref then Printer.pr_universe_instance sigma univs
+    else mt ()
+  in
+  hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_ltype_env env sigma typ ++ 
+  	   Printer.pr_universe_ctx sigma univs)
 
 (********************************)
 (** Printing implicit arguments *)
@@ -180,16 +187,16 @@ let print_opacity ref =
     | None -> []
     | Some s ->
        [pr_global ref ++ str " is " ++
-        str (match s with
-          | FullyOpaque -> "opaque"
+        match s with
+          | FullyOpaque -> str "opaque"
           | TransparentMaybeOpacified Conv_oracle.Opaque ->
-              "basically transparent but considered opaque for reduction"
+              str "basically transparent but considered opaque for reduction"
           | TransparentMaybeOpacified lev when Conv_oracle.is_transparent lev ->
-              "transparent"
+              str "transparent"
           | TransparentMaybeOpacified (Conv_oracle.Level n) ->
-              "transparent (with expansion weight "^string_of_int n^")"
+              str "transparent (with expansion weight " ++ int n ++ str ")"
           | TransparentMaybeOpacified Conv_oracle.Expand ->
-              "transparent (with minimal expansion weight)")]
+              str "transparent (with minimal expansion weight)"]
 
 (*******************)
 (* *)
@@ -205,16 +212,20 @@ let print_polymorphism ref =
        else "not universe polymorphic") ]
   else []
 
-let print_primitive_record mipv = function
+let print_primitive_record recflag mipv = function
   | Some (Some (_, ps,_)) ->
-    [pr_id mipv.(0).mind_typename ++ str" is primitive and has eta conversion."]
+    let eta = match recflag with
+    | Decl_kinds.CoFinite -> mt ()
+    | Decl_kinds.Finite | Decl_kinds.BiFinite -> str " and has eta conversion"
+    in
+    [pr_id mipv.(0).mind_typename ++ str" is primitive" ++ eta ++ str"."]
   | _ -> []
     
 let print_primitive ref =
   match ref with 
   | IndRef ind -> 
     let mib,_ = Global.lookup_inductive ind in
-      print_primitive_record mib.mind_packets mib.mind_record
+      print_primitive_record mib.mind_finite mib.mind_packets mib.mind_record
   | _ -> []
 
 let print_name_infos ref =
@@ -386,9 +397,9 @@ let print_located_qualid name flags ref =
     | [] ->
 	let (dir,id) = repr_qualid qid in
 	if DirPath.is_empty dir then
-	  str ("No " ^ name ^ " of basename") ++ spc () ++ pr_id id
+	  str "No " ++ str name ++ str " of basename" ++ spc () ++ pr_id id
 	else
-	  str ("No " ^ name ^ " of suffix") ++ spc () ++ pr_qualid qid
+	  str "No " ++ str name ++ str " of suffix" ++ spc () ++ pr_qualid qid
     | l ->
 	prlist_with_sep fnl
 	(fun (o,oqid) ->
@@ -447,7 +458,7 @@ let gallina_print_inductive sp =
   let mipv = mib.mind_packets in
   pr_mutual_inductive_body env sp mib ++
   with_line_skip
-    (print_primitive_record mipv mib.mind_record @
+    (print_primitive_record mib.mind_finite mipv mib.mind_record @
      print_inductive_renames sp mipv @
      print_inductive_implicit_args sp mipv @
      print_inductive_argument_scopes sp mipv)
@@ -459,16 +470,21 @@ let gallina_print_section_variable id =
   print_named_decl id ++
   with_line_skip (print_name_infos (VarRef id))
 
-let print_body = function
-  | Some c  -> pr_lconstr c
+let print_body env evd = function
+  | Some c  -> pr_lconstr_env env evd c
   | None -> (str"<no body>")
 
-let print_typed_body (val_0,typ) =
-  (print_body val_0 ++ fnl () ++ str "     : " ++ pr_ltype typ)
+let print_typed_body env evd (val_0,typ) =
+  (print_body env evd val_0 ++ fnl () ++ str "     : " ++ pr_ltype_env env evd typ)
 
 let ungeneralized_type_of_constant_type t = 
   Typeops.type_of_constant_type (Global.env ()) t
 
+let print_instance sigma cb =
+  if cb.const_polymorphic then
+    pr_universe_instance sigma cb.const_universes
+  else mt()
+				
 let print_constant with_values sep sp =
   let cb = Global.lookup_constant sp in
   let val_0 = Global.body_of_constant_body cb in
@@ -477,17 +493,23 @@ let print_constant with_values sep sp =
   let univs = Univ.instantiate_univ_context 
     (Global.universes_of_constant_body cb)
   in
+  let ctx =
+    Evd.evar_universe_context_of_binders
+      (Universes.universe_binders_of_global (ConstRef sp))
+  in
+  let env = Global.env () and sigma = Evd.from_ctx ctx in
+  let pr_ltype = pr_ltype_env env sigma in
   hov 0 (pr_polymorphic cb.const_polymorphic ++
     match val_0 with
     | None ->
 	str"*** [ " ++
-	print_basename sp ++ str " : " ++ cut () ++ pr_ltype typ ++
+	print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++
 	str" ]" ++
-	Printer.pr_universe_ctx univs
+	Printer.pr_universe_ctx sigma univs
     | _ ->
-	print_basename sp ++ str sep ++ cut () ++
-	(if with_values then print_typed_body (val_0,typ) else pr_ltype typ)++
-        Printer.pr_universe_ctx univs)
+	print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++
+	(if with_values then print_typed_body env sigma (val_0,typ) else pr_ltype typ)++
+        Printer.pr_universe_ctx sigma univs)
 
 let gallina_print_constant_with_infos sp =
   print_constant true " = " sp ++
diff --git a/printing/printer.ml b/printing/printer.ml
index 0d3a1c17..2e112f9a 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -208,10 +208,10 @@ let safe_pr_constr t =
   let (sigma, env) = get_current_context () in
   safe_pr_constr_env env sigma t
 
-let pr_universe_ctx c =
+let pr_universe_ctx sigma c =
   if !Detyping.print_universes && not (Univ.UContext.is_empty c) then
     fnl()++pr_in_comment (fun c -> v 0 
-      (Univ.pr_universe_context Universes.pr_with_global_universes c)) c
+      (Univ.pr_universe_context (Evd.pr_evd_level sigma) c)) c
   else
     mt()
 
@@ -455,14 +455,17 @@ let pr_ne_evar_set hd tl sigma l =
   else
     mt ()
 
+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 default_pr_subgoal n sigma =
   let rec prrec p = function
     | [] -> error "No such goal."
     | g::rest ->
 	if Int.equal p 1 then
-          let pg = default_pr_goal { sigma=sigma ; it=g; } in
-          v 0 (str "subgoal " ++ int n ++ pr_goal_tag g ++ pr_goal_name sigma g 
-	       ++ str " is:" ++ cut () ++ pg)
+          pr_selected_subgoal (int n) sigma g
 	else
 	  prrec (p-1) rest
   in
@@ -559,8 +562,8 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals
 	   ++ emacs_print_dependent_evars sigma seeds)
 	else
 	  let pei = pr_evars_int sigma 1 exl in
-	  (str "No more subgoals but non-instantiated existential " ++
-	   str "variables:" ++ fnl () ++ (hov 0 pei)
+	  (str "No more subgoals, but there are non-instantiated existential variables:"
+	   ++ fnl () ++ (hov 0 pei)
 	   ++ emacs_print_dependent_evars sigma seeds ++ fnl () ++
            str "You can use Grab Existential Variables.")
       end
@@ -625,17 +628,17 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
           begin match bgoals,shelf,given_up with
 	  | [] , [] , [] -> pr_subgoals None sigma seeds shelf stack goals
           | [] , [] , _ ->
-	     msg_info (str "No more goals, however there are goals you gave up. You need to go back and solve them.");
+	     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
+            ++ fnl () ++ str "You need to go back and solve them."
           | [] , _ , _ ->
 	    msg_info (str "All the remaining goals are on the shelf.");
 	    fnl ()
             ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] shelf
 	  | _ , _, _ ->
             let end_cmd =
-              strbrk "This subproof is complete, but there are still \
-              unfocused goals." ++
+              str "This subproof is complete, but there are some unfocused goals." ++
 	      (match Proof_global.Bullet.suggest p
               with None  -> str"" | Some s -> fnl () ++ str s) ++
               fnl ()
@@ -652,9 +655,17 @@ let pr_nth_open_subgoal n =
 
 let pr_goal_by_id id =
   let p = Proof_global.give_me_the_proof () in
-  let g = Goal.get_by_uid id in
+  try
+    Proof.in_proof p (fun sigma ->
+      let g = Evd.evar_key id sigma in
+      pr_selected_subgoal (pr_id id) sigma g)
+  with Not_found -> error "No such goal."
+
+let pr_goal_by_uid uid =
+  let p = Proof_global.give_me_the_proof () in
+  let g = Goal.get_by_uid uid in
   let pr gs =
-    v 0 (str ("goal / evar " ^ id ^ " is:") ++ cut ()
+    v 0 (str "goal / evar " ++ str uid ++ str " is:" ++ cut ()
 	 ++ pr_goal gs)
   in
   try
@@ -713,31 +724,72 @@ let prterm = pr_lconstr
 (* Printer function for sets of Assumptions.assumptions.
    It is used primarily by the Print Assumptions command. *)
 
-open Assumptions
+type context_object =
+  | Variable of Id.t (* A section variable or a Let definition *)
+  | Axiom of constant * (Label.t * Context.rel_context * types) list
+  | Opaque of constant     (* An opaque constant. *)
+  | Transparent of constant
+
+(* Defines a set of [assumption] *)
+module OrderedContextObject =
+struct
+  type t = context_object
+  let compare x y =
+      match x , y with
+      | Variable i1 , Variable i2 -> Id.compare i1 i2
+      | Axiom (k1,_) , Axiom (k2, _) -> con_ord k1 k2
+      | Opaque k1 , Opaque k2 -> con_ord k1 k2
+      | Transparent k1 , Transparent k2 -> con_ord k1 k2
+      | Axiom _ , Variable _ -> 1
+      | Opaque _ , Variable _
+      | Opaque _ , Axiom _ -> 1
+      | Transparent _ , Variable _
+      | Transparent _ , Axiom _
+      | Transparent _ , Opaque _ -> 1
+      | _ , _ -> -1
+end
+
+module ContextObjectSet = Set.Make (OrderedContextObject)
+module ContextObjectMap = Map.Make (OrderedContextObject)
 
 let pr_assumptionset env s =
-  if ContextObjectMap.is_empty s then
+  if ContextObjectMap.is_empty s &&
+       engagement env = (PredicativeSet, StratifiedType) then
     str "Closed under the global context"
   else
     let safe_pr_constant env kn =
       try pr_constant env kn
       with Not_found ->
 	let mp,_,lab = repr_con kn in
-	str (string_of_mp mp ^ "." ^ Label.to_string lab)
+        str (string_of_mp mp) ++ str "." ++ pr_label lab
     in
     let safe_pr_ltype typ =
       try str " : " ++ pr_ltype typ
       with e when Errors.noncritical e -> mt ()
     in
+    let safe_pr_ltype_relctx (rctx, typ) =
+      let sigma, env = get_current_context () in
+      let env = Environ.push_rel_context rctx env in
+      try str " " ++ pr_ltype_env env sigma typ
+      with e when Errors.noncritical e -> mt ()
+    in
     let fold t typ accu =
       let (v, a, o, tr) = accu in
       match t with
       | Variable id ->
         let var = str (Id.to_string id) ++ str " : " ++ pr_ltype typ in
         (var :: v, a, o, tr)
-      | Axiom kn ->
+      | Axiom (kn,[]) ->
         let ax = safe_pr_constant env kn ++ safe_pr_ltype typ in
         (v, ax :: a, o, tr)
+      | Axiom (kn,l) ->
+        let ax = safe_pr_constant env kn ++ safe_pr_ltype typ ++
+          cut() ++
+          prlist_with_sep cut (fun (lbl, ctx, ty) ->
+            str " used in " ++ str (Names.Label.to_string lbl) ++
+            str " to prove:" ++ safe_pr_ltype_relctx (ctx,ty))
+          l in
+        (v, ax :: a, o, tr)
       | Opaque kn ->
         let opq = safe_pr_constant env kn ++ safe_pr_ltype typ in
         (v, a, opq :: o, tr)
@@ -748,6 +800,16 @@ let pr_assumptionset env s =
     let (vars, axioms, opaque, trans) = 
       ContextObjectMap.fold fold s ([], [], [], [])
     in
+    let theory =
+      if is_impredicative_set env then
+	[str "Set is impredicative"]
+      else []
+    in
+    let theory =
+      if type_in_type env then
+	str "Type hierarchy is collapsed (logic is inconsistent)" :: theory
+      else theory
+    in
     let opt_list title = function
     | [] -> None
     | l ->
@@ -761,6 +823,7 @@ let pr_assumptionset env s =
       opt_list (str "Section Variables:") vars;
       opt_list (str "Axioms:") axioms;
       opt_list (str "Opaque constants:") opaque;
+      opt_list (str "Theory:") theory;
     ] in
     prlist_with_sep fnl (fun x -> x) (Option.List.flatten assums)
 
@@ -773,3 +836,7 @@ let pr_polymorphic b =
     if b then str"Polymorphic " else str"Monomorphic "
   else mt ()
 
+let pr_universe_instance evd ctx =
+  let inst = Univ.UContext.instance ctx in
+    str"@{" ++ Univ.Instance.pr (Evd.pr_evd_level evd) inst ++ str"}"
+
diff --git a/printing/printer.mli b/printing/printer.mli
index a469a8db..5c60b893 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -84,7 +84,8 @@ val pr_sort                : evar_map -> sorts -> std_ppcmds
 (** Universe constraints *)
 
 val pr_polymorphic         : bool -> std_ppcmds
-val pr_universe_ctx        : Univ.universe_context -> std_ppcmds
+val pr_universe_instance   : evar_map -> Univ.universe_context -> std_ppcmds
+val pr_universe_ctx        : evar_map -> Univ.universe_context -> std_ppcmds
 
 (** Printing global references using names as short as possible *)
 
@@ -160,12 +161,23 @@ val emacs_str              : string -> string
 val prterm                 : constr -> std_ppcmds (** = pr_lconstr *)
 
 
-(** spiwack: printer function for sets of Environ.assumption.
-            It is used primarily by the Print Assumption command. *)
+(** Declarations for the "Print Assumption" command *)
+type context_object =
+  | Variable of Id.t  (** A section variable or a Let definition *)
+  (** An axiom and the type it inhabits (if an axiom of the empty type) *)
+  | Axiom of constant * (Label.t * Context.rel_context * types) list
+  | Opaque of constant      (** An opaque constant. *)
+  | Transparent of constant (** A transparent constant *)
+
+module ContextObjectSet : Set.S with type elt = context_object
+module ContextObjectMap : CMap.ExtS
+  with type key = context_object and module Set := ContextObjectSet
+
 val pr_assumptionset :
-  env -> Term.types Assumptions.ContextObjectMap.t ->std_ppcmds
+  env -> Term.types ContextObjectMap.t -> std_ppcmds
 
-val pr_goal_by_id : string -> std_ppcmds
+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;
diff --git a/printing/printing.mllib b/printing/printing.mllib
index 7b4c71a8..652a34fa 100644
--- a/printing/printing.mllib
+++ b/printing/printing.mllib
@@ -1,6 +1,5 @@
 Genprint
 Pputils
-Ppstyle
 Ppannotation
 Ppconstr
 Ppconstrsig
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 295d8aaa..1d275c1a 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -72,10 +72,10 @@ let print_params env sigma params =
   if List.is_empty params then mt ()
   else Printer.pr_rel_context env sigma params ++ brk(1,2)
 
-let print_constructors envpar names types =
+let print_constructors envpar sigma names types =
   let pc =
     prlist_with_sep (fun () -> brk(1,0) ++ str "| ")
-      (fun (id,c) -> pr_id id ++ str " : " ++ Printer.pr_lconstr_env envpar Evd.empty c)
+      (fun (id,c) -> pr_id id ++ str " : " ++ Printer.pr_lconstr_env envpar sigma c)
       (Array.to_list (Array.map2 (fun n t -> (n,t)) names types))
   in
   hv 0 (str "  " ++ pc)
@@ -83,7 +83,7 @@ let print_constructors envpar names types =
 let build_ind_type env mip =
   Inductive.type_of_inductive env mip
 
-let print_one_inductive env mib ((_,i) as ind) =
+let print_one_inductive env sigma mib ((_,i) as ind) =
   let u = if mib.mind_polymorphic then 
       Univ.UContext.instance mib.mind_universes 
     else Univ.Instance.empty in
@@ -94,10 +94,15 @@ let print_one_inductive env mib ((_,i) as ind) =
   let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in
   let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in
   let envpar = push_rel_context params env in
+  let inst =
+    if mib.mind_polymorphic then
+      Printer.pr_universe_instance sigma mib.mind_universes
+    else mt ()
+  in
   hov 0 (
-    pr_id mip.mind_typename ++ brk(1,4) ++ print_params env Evd.empty params ++
-    str ": " ++ Printer.pr_lconstr_env envpar Evd.empty arity ++ str " :=") ++
-  brk(0,2) ++ print_constructors envpar mip.mind_consnames cstrtypes
+    pr_id mip.mind_typename ++ inst ++ brk(1,4) ++ print_params env sigma params ++
+    str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ str " :=") ++
+  brk(0,2) ++ print_constructors envpar sigma mip.mind_consnames cstrtypes
 
 let print_mutual_inductive env mind mib =
   let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x))
@@ -109,11 +114,13 @@ let print_mutual_inductive env mind mib =
     | BiFinite -> "Variant"
     | CoFinite -> "CoInductive"
   in
+  let bl = Universes.universe_binders_of_global (IndRef (mind, 0)) in
+  let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
   hov 0 (Printer.pr_polymorphic mib.mind_polymorphic ++
     def keyword ++ spc () ++
     prlist_with_sep (fun () -> fnl () ++ str"  with ")
-      (print_one_inductive env mib) inds ++
-      Printer.pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes))
+      (print_one_inductive env sigma mib) inds ++
+      Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes))
 
 let get_fields =
   let rec prodec_rec l subst c =
@@ -142,6 +149,8 @@ let print_record env mind mib =
   let cstrtype = hnf_prod_applist env cstrtypes.(0) args in
   let fields = get_fields cstrtype in
   let envpar = push_rel_context params env in
+  let bl = Universes.universe_binders_of_global (IndRef (mind,0)) in
+  let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
   let keyword =
     let open Decl_kinds in
     match mib.mind_finite with
@@ -153,16 +162,16 @@ let print_record env mind mib =
     hov 0 (
       Printer.pr_polymorphic mib.mind_polymorphic ++
       def keyword ++ spc () ++ pr_id mip.mind_typename ++ brk(1,4) ++
-      print_params env Evd.empty params ++
-      str ": " ++ Printer.pr_lconstr_env envpar Evd.empty arity ++ brk(1,2) ++
+      print_params env sigma params ++
+      str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ brk(1,2) ++
       str ":= " ++ pr_id mip.mind_consnames.(0)) ++
     brk(1,2) ++
     hv 2 (str "{ " ++
       prlist_with_sep (fun () -> str ";" ++ brk(2,0))
         (fun (id,b,c) ->
           pr_id id ++ str (if b then " : " else " := ") ++
-          Printer.pr_lconstr_env envpar Evd.empty c) fields) ++ str" }" ++
-      Printer.pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes))
+          Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++
+      Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes))
 
 let pr_mutual_inductive_body env mind mib =
   if mib.mind_record <> None && not !Flags.raw_print then
@@ -259,6 +268,11 @@ let print_body is_impl env mp (l,body) =
     | SFBmodule _ -> keyword "Module" ++ spc () ++ name
     | SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name
     | SFBconst cb ->
+       let u =
+	 if cb.const_polymorphic then Univ.UContext.instance cb.const_universes
+	 else Univ.Instance.empty
+       in
+       let sigma = Evd.empty in
       (match cb.const_body with
 	| Def _ -> def "Definition" ++ spc ()
 	| OpaqueDef _ when is_impl -> def "Theorem" ++ spc ()
@@ -267,15 +281,17 @@ let print_body is_impl env mp (l,body) =
 	  | None -> mt ()
 	  | Some env ->
 	    str " :" ++ spc () ++
-	    hov 0 (Printer.pr_ltype_env env Evd.empty (* No evars in modules *)
-		     (Typeops.type_of_constant_type env cb.const_type)) ++
+	    hov 0 (Printer.pr_ltype_env env sigma
+		(Vars.subst_instance_constr u
+   		  (Typeops.type_of_constant_type env cb.const_type))) ++
 	    (match cb.const_body with
 	      | Def l when is_impl ->
 		spc () ++
 		hov 2 (str ":= " ++
-		       Printer.pr_lconstr_env env Evd.empty (Mod_subst.force_constr l))
+		       Printer.pr_lconstr_env env sigma
+			  (Vars.subst_instance_constr u (Mod_subst.force_constr l)))
 	      | _ -> mt ()) ++ str "." ++
-	    Printer.pr_universe_ctx cb.const_universes)
+	    Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context cb.const_universes))
     | SFBmind mib ->
       try
 	let env = Option.get env in
@@ -315,15 +331,17 @@ let rec print_typ_expr env mp locals mty =
       let mapp = List.tl lapp in
       hov 3 (str"(" ++ (print_kn locals fapp) ++ spc () ++
 		 prlist_with_sep spc (print_modpath locals) mapp ++ str")")
-  | MEwith(me,WithDef(idl,c))->
+  | MEwith(me,WithDef(idl,(c, _)))->
       let env' = None in (* TODO: build a proper environment if env <> None *)
       let s = String.concat "." (List.map Id.to_string idl) in
       hov 2 (print_typ_expr env' mp locals me ++ spc() ++ str "with" ++ spc()
-             ++ def "Definition"++ spc() ++ str s ++ spc() ++  str ":="++ spc())
-  | MEwith(me,WithMod(idl,mp))->
+             ++ def "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc()
+             ++ Printer.pr_lconstr c)
+  | MEwith(me,WithMod(idl,mp'))->
       let s = String.concat "." (List.map Id.to_string idl) in
       hov 2 (print_typ_expr env mp locals me ++ spc() ++ str "with" ++ spc() ++
-             keyword "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc())
+             keyword "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc()
+             ++ print_modpath locals mp')
 
 let print_mod_expr env mp locals = function
   | MEident mp -> print_modpath locals mp