Moving mutual inductive printing from Printer to Printmod.

1 files changed, 0 insertions, 106 deletions

diff --git a/printing/printer.ml b/printing/printer.ml
index e21c9a61b9..8a906b3f15 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -768,109 +768,3 @@ let pr_polymorphic b =
     if b then str"Polymorphic " else str"Monomorphic "
   else mt ()
 
-(** Inductive declarations *)
-
-open Termops
-open Reduction
-
-let print_params env sigma params =
-  if List.is_empty params then mt ()
-  else pr_rel_context env sigma params ++ brk(1,2)
-
-let print_constructors envpar names types =
-  let pc =
-    prlist_with_sep (fun () -> brk(1,0) ++ str "| ")
-      (fun (id,c) -> pr_id id ++ str " : " ++ pr_lconstr_env envpar Evd.empty c)
-      (Array.to_list (Array.map2 (fun n t -> (n,t)) names types))
-  in
-  hv 0 (str "  " ++ pc)
-
-let build_ind_type env mip =
-  Inductive.type_of_inductive env mip
-
-let print_one_inductive env mib ((_,i) as ind) =
-  let u = if mib.mind_polymorphic then 
-      Univ.UContext.instance mib.mind_universes 
-    else Univ.Instance.empty in
-  let mip = mib.mind_packets.(i) in
-  let params = Inductive.inductive_paramdecls (mib,u) in
-  let args = extended_rel_list 0 params in
-  let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in
-  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
-  hov 0 (
-    pr_id mip.mind_typename ++ brk(1,4) ++ print_params env Evd.empty params ++
-    str ": " ++ pr_lconstr_env envpar Evd.empty arity ++ str " :=") ++
-  brk(0,2) ++ print_constructors envpar mip.mind_consnames cstrtypes
-
-let print_mutual_inductive env mind mib =
-  let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x))
-  in
-  let keyword =
-    let open Decl_kinds in
-    match mib.mind_finite with
-    | Finite -> "Inductive "
-    | BiFinite -> "Variant "
-    | CoFinite -> "CoInductive "
-  in
-  hov 0 (pr_polymorphic mib.mind_polymorphic ++
-    str keyword ++
-    prlist_with_sep (fun () -> fnl () ++ str"  with ")
-      (print_one_inductive env mib) inds ++
-      pr_universe_ctx (Univ.instantiate_univ_context mib.mind_universes))
-
-let get_fields =
-  let rec prodec_rec l subst c =
-    match kind_of_term c with
-    | Prod (na,t,c) ->
-	let id = match na with Name id -> id | Anonymous -> Id.of_string "_" in
-	prodec_rec ((id,true,substl subst t)::l) (mkVar id::subst) c
-    | LetIn (na,b,_,c) ->
-	let id = match na with Name id -> id | Anonymous -> Id.of_string "_" in
-	prodec_rec ((id,false,substl subst b)::l) (mkVar id::subst) c
-    | _               -> List.rev l
-  in
-  prodec_rec [] []
-
-let print_record env mind mib =
-  let u = 
-    if mib.mind_polymorphic then 
-      Univ.UContext.instance mib.mind_universes 
-    else Univ.Instance.empty 
-  in
-  let mip = mib.mind_packets.(0) in
-  let params = Inductive.inductive_paramdecls (mib,u) in
-  let args = extended_rel_list 0 params in
-  let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in
-  let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (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
-  let keyword =
-    let open Decl_kinds in
-    match mib.mind_finite with
-    | BiFinite -> "Record "
-    | Finite -> "Inductive "
-    | CoFinite -> "CoInductive "
-  in
-  hov 0 (
-    hov 0 (
-      pr_polymorphic mib.mind_polymorphic ++
-      str keyword ++ pr_id mip.mind_typename ++ brk(1,4) ++
-      print_params env Evd.empty params ++
-      str ": " ++ pr_lconstr_env envpar Evd.empty 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 " := ") ++
-	  pr_lconstr_env envpar Evd.empty c) fields) ++ str" }" ++
-      pr_universe_ctx (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
-    print_record env mind mib
-  else
-    print_mutual_inductive env mind mib