Merge branch 'v8.5'

4 files changed, 62 insertions, 29 deletions

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index b8c5fd4cfc..84649e6ebf 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 *)
@@ -463,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
@@ -481,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 18e4902255..202b4f2bc7 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()
 
@@ -825,3 +825,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 5f56adbe6f..0a44e4f103 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 *)
 
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 53d0508c7f..1d275c1aa6 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
@@ -263,6 +272,7 @@ let print_body is_impl env mp (l,body) =
 	 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 ()
@@ -271,17 +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 *)
+	    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
+		       Printer.pr_lconstr_env env sigma
 			  (Vars.subst_instance_constr u (Mod_subst.force_constr l)))
 	      | _ -> mt ()) ++ str "." ++
-	    Printer.pr_universe_ctx (Univ.instantiate_univ_context cb.const_universes))
+	    Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context cb.const_universes))
     | SFBmind mib ->
       try
 	let env = Option.get env in