Deactivating printing of {| |} for records when option Printing All is set.

Simplifying the printing of "in" clause keeping the same defaults as
in parsing (e.g. "simpl" is printed "simpl" and not "simpl in *").

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

2 files changed, 15 insertions, 9 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 60960754b1..550155ee30 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -405,6 +405,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
       let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
       let p =
 	try
+	  if !Flags.raw_print then raise Exit;
 	  let projs = Recordops.lookup_projections (fst cstrsp) in
 	  let rec ip projs args acc =
 	    match projs with
@@ -420,7 +421,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
 	    in
 	  CPatRecord(loc, List.rev (ip projs args []))
 	with
-	  Not_found | No_match ->
+	  Not_found | No_match | Exit ->
 	    CPatCstr (loc, extern_reference loc vars (ConstructRef cstrsp), args) in
       insert_pat_alias loc p na
 
@@ -656,6 +657,7 @@ let rec extern inctx scopes vars r =
 	       extern_args (extern true) (snd scopes) vars args subscopes in
 	     begin
 	       try
+		 if !Flags.raw_print then raise Exit;
 		 let cstrsp = match ref with ConstructRef c -> c | _ -> raise Not_found in
 		 let struc = Recordops.lookup_structure (fst cstrsp) in
 		 let projs = struc.Recordops.s_PROJ in
@@ -682,7 +684,7 @@ let rec extern inctx scopes vars r =
 		   in
 		 CRecord (loc, None, List.rev (ip projs locals args []))
 	       with
-		 | Not_found | No_match ->
+		 | Not_found | No_match | Exit ->
 		     extern_app loc inctx (implicits_of_global ref)
 		       (Some ref,extern_reference rloc vars ref) args
 	     end
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 9d68f1cd9e..1fde7b245a 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -426,7 +426,11 @@ let pr_in_hyp_as pr_id = function
   | None -> mt ()
   | Some (id,ipat) -> pr_simple_hyp_clause pr_id [id] ++ pr_as_ipat ipat
 
-let pr_clauses pr_id = function
+let pr_clauses default_is_concl pr_id = function
+  | { onhyps=Some []; concl_occs=occs }
+      when occs = all_occurrences_expr & default_is_concl = Some true -> mt ()
+  | { onhyps=None; concl_occs=occs }
+      when occs = all_occurrences_expr & default_is_concl = Some false -> mt ()
   | { onhyps=None; concl_occs=occs } ->
       if occs = no_occurrences_expr then pr_in (str " * |-")
       else pr_in (pr_with_occurrences (fun () -> str " *") (occs,()))
@@ -737,7 +741,7 @@ and pr_atom1 = function
       hov 1 ((if b then str "set" else str "remember") ++
              (if b then pr_pose pr_lconstr else pr_pose_as_style)
 	        pr_constr na c ++
-             pr_clauses pr_ident cl)
+             pr_clauses (Some b) pr_ident cl)
 (*  | TacInstantiate (n,c,ConclLocation ()) ->
       hov 1 (str "instantiate" ++ spc() ++
              hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
@@ -759,7 +763,7 @@ and pr_atom1 = function
 	       prlist_with_sep spc (pr_induction_arg pr_lconstr pr_constr) h ++
 	       pr_with_induction_names ids ++
                pr_opt pr_eliminator e) l ++
-               pr_opt_no_spc (pr_clauses pr_ident) cl)
+               pr_opt_no_spc (pr_clauses None pr_ident) cl)
   | TacDoubleInduction (h1,h2) ->
       hov 1
         (str "double induction" ++
@@ -831,7 +835,7 @@ and pr_atom1 = function
   (* Conversion *)
   | TacReduce (r,h) ->
       hov 1 (pr_red_expr r ++
-             pr_clauses pr_ident h)
+             pr_clauses (Some true) pr_ident h)
   | TacChange (occ,c,h) ->
       hov 1 (str "change" ++ brk (1,1) ++
       (match occ with
@@ -839,11 +843,11 @@ and pr_atom1 = function
         | Some occlc ->
 	    pr_with_occurrences_with_trailer pr_constr occlc
 	      (spc () ++ str "with ")) ++
-      pr_constr c ++ pr_clauses pr_ident h)
+      pr_constr c ++ pr_clauses (Some true) pr_ident h)
 
   (* Equivalence relations *)
   | TacReflexivity as x -> pr_atom0 x
-  | TacSymmetry cls -> str "symmetry " ++ pr_clauses pr_ident cls
+  | TacSymmetry cls -> str "symmetry " ++ pr_clauses (Some true) pr_ident cls
   | TacTransitivity (Some c) -> str "transitivity" ++ pr_constrarg c
   | TacTransitivity None -> str "etransitivity"
 
@@ -855,7 +859,7 @@ and pr_atom1 = function
 	     (fun (b,m,c) ->
 		pr_orient b ++ spc() ++ pr_multi m ++ pr_with_bindings c)
 	     l
-	     ++ pr_clauses pr_ident cl
+	     ++ pr_clauses (Some true) pr_ident cl
 	     ++	(match by with Some by -> pr_by_tactic (pr_tac_level ltop) by | None -> mt()))
   | TacInversion (DepInversion (k,c,ids),hyp) ->
       hov 1 (str "dependent " ++ pr_induction_kind k ++ spc () ++