Passage de lconstr à constr pour les arguments immédiat de commandes

et tactiques; qqes bugs d'affichage; passage de la précédence des
projections de 10 à 9 avec associativité à gauche


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

3 files changed, 38 insertions, 27 deletions

diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index a343b37a60..a03207f254 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -40,7 +40,8 @@ let lfix = 200
 let larrow = 80
 let lnegint = 40
 let lcast = 100
-let lapp = 1
+let lapp = 10
+let lproj = 9
 let ltop = (200,E)
 let lsimple = (0,E)
 
@@ -365,7 +366,7 @@ let pr_simple_return_type pr na po =
   pr_case_type pr po
 
 let pr_proj pr pr_app a f l =
-  hov 0 (pr lsimple a ++ cut() ++ str ".(" ++ pr_app pr f l ++ str ")")
+  hov 0 (pr (lproj,E) a ++ cut() ++ str ".(" ++ pr_app pr f l ++ str ")")
 
 let pr_appexpl pr f l =
       hov 2 (
@@ -410,15 +411,21 @@ let rec pr inherited a =
   | CAppExpl (_,(Some i,f),l) ->
       let l1,l2 = list_chop i l in
       let c,l1 = list_sep_last l1 in
-      pr_proj pr pr_appexpl c f l1 ++
-      prlist (fun a -> spc () ++ pr (lapp,L) a) l2, lapp
+      let p = pr_proj pr pr_appexpl c f l1 in
+      if l2<>[] then
+	p ++ prlist (fun a -> spc () ++ pr (lapp,L) a) l2, lapp
+      else
+	p, lproj
   | CAppExpl (_,(None,f),l) -> pr_appexpl pr f l, lapp
   | CApp (_,(Some i,f),l) ->
       let l1,l2 = list_chop i l in
       let c,l1 = list_sep_last l1 in
       assert (snd c = None);
-      pr_proj pr pr_app (fst c) f l1 ++
-      prlist (fun a -> spc () ++ pr_expl_args pr a) l2, lapp
+      let p = pr_proj pr pr_app (fst c) f l1 in
+      if l2<>[] then 
+	p ++ prlist (fun a -> spc () ++ pr_expl_args pr a) l2, lapp
+      else
+	p, lproj
   | CApp (_,(None,a),l) -> pr_app pr a l, lapp
   | CCases (_,(po,rtntypopt),c,eqns) ->
       v 0
@@ -589,12 +596,12 @@ let rec pr_may_eval prc prlc pr2 = function
       hov 0
         (str "eval" ++ brk (1,1) ++
          pr_red_expr (prc,prlc,pr2) r ++
-	 str " in" ++ spc() ++ prlc c)
+	 str " in" ++ spc() ++ prc c)
   | ConstrContext ((_,id),c) ->
       hov 0
 	(str "inst " ++ pr_id id ++ spc () ++
 	 str "[" ++ prlc c ++ str "]")
-  | ConstrTypeOf c -> hov 1 (str "check" ++ spc() ++ prlc c)
+  | ConstrTypeOf c -> hov 1 (str "check" ++ spc() ++ prc c)
   | ConstrTerm c -> prlc c
 
 let pr_rawconstr_env_no_translate env c =
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index a701efea38..a03a8c2466 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -222,14 +222,14 @@ and pr_atom1 env = function
       hov 1
       (str "intro" ++ pr_opt pr_id ido1 ++ spc () ++ str "after " ++ pr_id id2)
   | TacAssumption as t -> pr_atom0 env t
-  | TacExact c -> hov 1 (str "exact" ++ pr_lconstrarg env c)
+  | TacExact c -> hov 1 (str "exact" ++ pr_constrarg env c)
   | TacApply cb -> hov 1 (str "apply" ++ spc () ++ pr_with_bindings env cb)
   | TacElim (cb,cbo) ->
       hov 1 (str "elim" ++ pr_arg (pr_with_bindings env) cb ++ 
         pr_opt (pr_eliminator env) cbo)
-  | TacElimType c -> hov 1 (str "elimtype" ++ pr_lconstrarg env c)
+  | TacElimType c -> hov 1 (str "elimtype" ++ pr_constrarg env c)
   | TacCase cb -> hov 1 (str "case" ++ spc () ++ pr_with_bindings env cb)
-  | TacCaseType c -> hov 1 (str "CaseType" ++ pr_lconstrarg env c)
+  | TacCaseType c -> hov 1 (str "casetype" ++ pr_constrarg env c)
   | TacFix (ido,n) -> hov 1 (str "fix" ++ pr_opt pr_id ido ++ pr_intarg n)
   | TacMutualFix (id,n,l) ->
       hov 1 (str "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc () ++
@@ -248,24 +248,26 @@ and pr_atom1 env = function
 	      spc() ++ 
 	      hov 0 (pr_id id ++ str":" ++ pr_constrarg env c))
 	  l))
-  | TacCut c -> hov 1 (str "cut" ++ pr_lconstrarg env c)
+  | TacCut c -> hov 1 (str "cut" ++ pr_constrarg env c)
   | TacTrueCut (None,c) -> 
-      hov 1 (str "assert" ++ pr_lconstrarg env c)
+      hov 1 (str "assert" ++ pr_constrarg env c)
   | TacTrueCut (Some id,c) -> 
       hov 1 (str "assert" ++ spc () ++ pr_id id ++ str ":" ++
              pr_lconstrarg env c)
   | TacForward (false,na,c) ->
       hov 1 (str "assert" ++ pr_arg pr_name na ++ str " :=" ++
              pr_lconstrarg env c)
-  | TacForward (true,na,c) ->
-      hov 1 (str "pose" ++ pr_arg pr_name na ++ str " :=" ++
+  | TacForward (true,Anonymous,c) ->
+      hov 1 (str "pose" ++ pr_constrarg env c)
+  | TacForward (true,Name id,c) ->
+      hov 1 (str "pose" ++ pr_arg pr_id id ++ str " :=" ++
              pr_lconstrarg env c)
   | TacGeneralize l ->
       hov 1 (str "generalize" ++ spc () ++
              prlist_with_sep spc (pr_constr env) l)
   | TacGeneralizeDep c ->
       hov 1 (str "generalize" ++ spc () ++ str "dependent" ++
-             pr_lconstrarg env c)
+             pr_constrarg env c)
   | TacLetTac (id,c,cl) ->
       hov 1 (str "lettac" ++ spc () ++ pr_id id ++ str " :=" ++
         pr_constrarg env c ++ pr_clause_pattern pr_ident cl)
@@ -277,13 +279,13 @@ and pr_atom1 env = function
       hov 1 (str "oldinduction" ++ pr_arg pr_quantified_hypothesis h)
   | TacNewInduction (h,e,ids) ->
       hov 1 (str "induction" ++ spc () ++
-             pr_induction_arg (pr_lconstr env) h ++
+             pr_induction_arg (pr_constr env) h ++
              pr_opt (pr_eliminator env) e ++ pr_with_names ids)
   | TacOldDestruct h ->
       hov 1 (str "olddestruct" ++ pr_arg pr_quantified_hypothesis h)
   | TacNewDestruct (h,e,ids) ->
       hov 1 (str "destruct" ++ spc () ++
-             pr_induction_arg (pr_lconstr env) h ++
+             pr_induction_arg (pr_constr env) h ++
              pr_opt (pr_eliminator env) e ++ pr_with_names ids)
   | TacDoubleInduction (h1,h2) ->
       hov 1
@@ -291,18 +293,18 @@ and pr_atom1 env = function
          pr_arg pr_quantified_hypothesis h1 ++
  	 pr_arg pr_quantified_hypothesis h2)
   | TacDecomposeAnd c ->
-      hov 1 (str "decompose record" ++ pr_lconstrarg env c)
+      hov 1 (str "decompose record" ++ pr_constrarg env c)
   | TacDecomposeOr c ->
-      hov 1 (str "decompose sum" ++ pr_lconstrarg env c)
+      hov 1 (str "decompose sum" ++ pr_constrarg env c)
   | TacDecompose (l,c) ->
       let vars = Termops.vars_of_env env in
       hov 1 (str "decompose" ++ spc () ++
         hov 0 (str "[" ++ prlist_with_sep spc (pr_ind vars) l
-	  ++ str "]" ++ pr_lconstrarg env c))
+	  ++ str "]" ++ pr_constrarg env c))
   | TacSpecialize (n,c) ->
       hov 1 (str "specialize" ++ spc () ++ pr_opt int n ++ pr_with_bindings env c)
   | TacLApply c -> 
-      hov 1 (str "lapply" ++ pr_lconstrarg env c)
+      hov 1 (str "lapply" ++ pr_constrarg env c)
 
   (* Automation tactics *)
   | TacTrivial (Some []) as x -> pr_atom0 env x
@@ -368,7 +370,7 @@ and pr_atom1 env = function
   (* Equivalence relations *)
   | (TacReflexivity | TacSymmetry None) as x -> pr_atom0 env x
   | TacSymmetry (Some id) -> str "symmetry in " ++ pr_ident id
-  | TacTransitivity c -> str "transitivity" ++ pr_lconstrarg env c in
+  | TacTransitivity c -> str "transitivity" ++ pr_constrarg env c in
 
 let ltop = (5,E) in
 let lseq = 5 in
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 491b8ab497..f5966a5ccc 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -1008,10 +1008,12 @@ pr_vbinders bl ++ spc())
       | Some r0 ->
           hov 2 (str"Eval" ++ spc() ++
           pr_red_expr (pr_constr,pr_lconstr,pr_reference) r0 ++
-          spc() ++ str"in" ++ spc () ++ pr_lconstr c)
-      | None -> hov 2 (str"Check" ++ spc() ++ pr_lconstr c) 
-      in pr_mayeval r c
-  | VernacGlobalCheck c -> hov 2 (str"Type" ++ pr_lconstrarg c)
+          spc() ++ str"in" ++ spc () ++ pr_constr c)
+      | None -> hov 2 (str"Check" ++ spc() ++ pr_constr c) 
+      in 
+      (if io = None then mt() else int (out_some io) ++ str ": ") ++ 
+      pr_mayeval r c
+  | VernacGlobalCheck c -> hov 2 (str"Type" ++ pr_constrarg c)
   | VernacPrint p -> 
       let pr_printable = function
 	| PrintFullContext -> str"Print All"