Restore display of notation when printing an inductive such as sig

 + minor pp improvement for Print Module Type

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14148 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 29 insertions, 41 deletions

diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 4d35ac708..38c8a7438 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -339,7 +339,7 @@ let gallina_print_inductive sp =
   let env = Global.env() in
   let mib = Environ.lookup_mind sp env in
   let mipv = mib.mind_packets in
-  pr_mutual_inductive_body env mib ++ fnl () ++
+  pr_mutual_inductive_body env sp mib ++ fnl () ++
   with_line_skip
     (print_inductive_implicit_args sp mipv @
      print_inductive_argument_scopes sp mipv)
@@ -531,7 +531,7 @@ let print_full_pure_context () =
       | "INDUCTIVE" ->
 	  let mind = Global.mind_of_delta (mind_of_kn kn) in
 	  let mib = Global.lookup_mind mind in
-	  pr_mutual_inductive_body (Global.env()) mib ++
+	  pr_mutual_inductive_body (Global.env()) mind mib ++
 	    str "." ++ fnl () ++ fnl ()
       | "MODULE" ->
 	  (* TODO: make it reparsable *)
diff --git a/parsing/printer.ml b/parsing/printer.ml
index d9b6d8082..10ccd879b 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -565,34 +565,26 @@ let build_ind_type env mip =
     | Polymorphic ar ->
       it_mkProd_or_LetIn (mkSort (Type ar.poly_level)) mip.mind_arity_ctxt
 
-let print_one_inductive env mib (mip,ind_typ) =
+let print_one_inductive env mib ((_,i) as ind) =
+  let mip = mib.mind_packets.(i) in
   let params = mib.mind_params_ctxt in
-  (* In case of lets in params, mind_nparams <> List.length params *)
-  let lparams = List.length params in
   let args = extended_rel_list 0 params in
-  let arity = hnf_prod_applist env ind_typ args in
+  let arity = hnf_prod_applist env (build_ind_type env mip) args in
+  let cstrtypes = Inductive.type_of_constructors ind (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 cstrtypes =
-    Array.map (fun c -> hnf_prod_applist envpar (lift lparams c) args)
-      mip.mind_user_lc
-  in
   hov 0 (
     pr_id mip.mind_typename ++ brk(1,4) ++ print_params env params ++
     str ": " ++ pr_lconstr_env envpar arity ++ str " :=") ++
   brk(0,2) ++ print_constructors envpar mip.mind_consnames cstrtypes
 
-let print_mutual_inductive env mib =
-  let mips = Array.to_list mib.mind_packets in
-  let ind_types = List.map (build_ind_type env) mips in
-  let mips_types = List.combine mips ind_types in
-  let ind_ctxt =
-    List.rev_map (fun (m,t) -> (Name m.mind_typename, None, t)) mips_types
+let print_mutual_inductive env mind mib =
+  let inds = list_tabulate (fun x -> (mind,x)) (Array.length mib.mind_packets)
   in
-  let envind = push_rel_context ind_ctxt env in
   hov 0 (
     str (if mib.mind_finite then "Inductive " else "CoInductive ") ++
     prlist_with_sep (fun () -> fnl () ++ str"  with ")
-      (print_one_inductive envind mib) mips_types)
+      (print_one_inductive env mib) inds)
 
 let get_fields =
   let rec prodec_rec l subst c =
@@ -607,23 +599,18 @@ let get_fields =
   in
   prodec_rec [] []
 
-let print_record env mib =
+let print_record env mind mib =
   let mip = mib.mind_packets.(0) in
-  let ind_typ = build_ind_type env mip in
-  let ind_name = mip.mind_typename in
-  let envind = push_rel_context [(Name ind_name, None, ind_typ)] env in
   let params = mib.mind_params_ctxt in
-  let lparams = List.length params in
   let args = extended_rel_list 0 params in
-  let arity = hnf_prod_applist env ind_typ args in
-  let envpar = push_rel_context params envind in
-  let cstr_typ =
-    hnf_prod_applist envpar (lift lparams mip.mind_user_lc.(0)) args
-  in
-  let fields = get_fields cstr_typ in
+  let arity = hnf_prod_applist env (build_ind_type env mip) args in
+  let cstrtypes = Inductive.type_of_constructors (mind,0) (mib,mip) in
+  let cstrtype = hnf_prod_applist env cstrtypes.(0) args in
+  let fields = get_fields cstrtype in
+  let envpar = push_rel_context params env in
   hov 0 (
     hov 0 (
-      str "Record " ++ pr_id ind_name ++ brk(1,4) ++
+      str "Record " ++ pr_id mip.mind_typename ++ brk(1,4) ++
       print_params env params ++
       str ": " ++ pr_lconstr_env envpar arity ++ brk(1,2) ++
       str ":= " ++ pr_id mip.mind_consnames.(0)) ++
@@ -634,8 +621,8 @@ let print_record env mib =
 	  pr_id id ++ str (if b then " : " else " := ") ++
 	  pr_lconstr_env envpar c) fields) ++ str" }")
 
-let pr_mutual_inductive_body env mib =
+let pr_mutual_inductive_body env mind mib =
   if mib.mind_record & not !Flags.raw_print then
-    print_record env mib
+    print_record env mind mib
   else
-    print_mutual_inductive env mib
+    print_mutual_inductive env mind mib
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 713484a76..b4e0537a5 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -147,4 +147,4 @@ val pr_instance_gmap : (global_reference, Typeclasses.instance Names.Cmap.t) Gma
 (** Inductive declarations *)
 
 val pr_mutual_inductive_body :
-  env -> Declarations.mutual_inductive_body -> std_ppcmds
+  env -> mutual_inductive -> Declarations.mutual_inductive_body -> std_ppcmds
diff --git a/parsing/printmod.ml b/parsing/printmod.ml
index f258da587..cf2aad203 100644
--- a/parsing/printmod.ml
+++ b/parsing/printmod.ml
@@ -124,7 +124,7 @@ let print_body is_impl env mp (l,body) =
     | SFBmind mib ->
       try
 	let env = Option.get env in
-	Printer.pr_mutual_inductive_body env mib
+	Printer.pr_mutual_inductive_body env (make_mind mp empty_dirpath l) mib
       with _ ->
 	(if mib.mind_finite then str "Inductive " else str "CoInductive")
 	++ name)
@@ -248,9 +248,10 @@ let print_module with_body mp =
 let print_modtype kn =
   let mtb = Global.lookup_modtype kn in
   let name = print_kn [] kn in
-  str "Module Type " ++ name ++ str " = " ++
-  (try
-     if !short then raise ShortPrinting;
-     print_modtype' (Some (Global.env ())) kn mtb.typ_expr
-   with _ ->
-     print_modtype' None kn mtb.typ_expr)
+  hv 1
+    (str "Module Type " ++ name ++ str " =" ++ spc () ++
+     (try
+	if !short then raise ShortPrinting;
+	print_modtype' (Some (Global.env ())) kn mtb.typ_expr
+      with _ ->
+	print_modtype' None kn mtb.typ_expr))