Réaffichage des Structure/Record sous la forme Record

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

2 files changed, 36 insertions, 1 deletions

diff --git a/CHANGES b/CHANGES
index b1d42a03a8..afcffda32c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -23,6 +23,7 @@ Notations and implicit arguments
 - New modifier in "Implicit Arguments" to force an implicit argument to
   be maximally inserted.
 - Level "constr" moved from 9 to 8.
+- Structure/Record now printed as Record (unless option Printing All is set).
 
 Tactic Language
 
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 4d311b177b..9acf697e32 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -320,11 +320,45 @@ let pr_mutual_inductive finite indl =
     prlist_with_sep (fun () -> fnl () ++ str"  with ")
       print_one_inductive indl)
 
+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
+    | _               -> l
+  in 
+  prodec_rec [] []
+
+let pr_record (sp,tyi) =
+  let (ref, params, arity, cstrnames, cstrtypes) = build_inductive sp tyi in
+  let env = Global.env () in
+  let envpar = push_rel_context params env in
+  let fields = get_fields cstrtypes.(0) in
+  hov 0 (
+    hov 0 (
+      str "Record " ++ pr_global (IndRef (sp,tyi)) ++ brk(1,4) ++ 
+      print_params env params ++
+      str ": " ++ pr_lconstr_env envpar arity ++ brk(1,2) ++ 
+      str ":= " ++ pr_id cstrnames.(0)) ++ 
+    brk(1,2) ++
+    hv 2 (str "{ " ++
+      prlist_with_sep (fun () -> str "; " ++ brk(1,0))
+        (fun (id,b,c) -> 
+	  pr_id id ++ str (if b then " : " else " := ") ++ 
+	  pr_lconstr_env envpar c) fields) ++ str" }")
+
 let gallina_print_inductive sp =
   let (mib,mip) = Global.lookup_inductive (sp,0) in
   let mipv = mib.mind_packets in
   let names = list_tabulate (fun x -> (sp,x)) (Array.length mipv) in
-  pr_mutual_inductive mib.mind_finite names ++ fnl () ++ fnl () ++
+  (if mib.mind_record & not !Options.raw_print then
+    pr_record (List.hd names)
+  else
+    pr_mutual_inductive mib.mind_finite names) ++ fnl () ++ fnl () ++
   print_inductive_implicit_args sp mipv ++
   print_inductive_argument_scopes sp mipv