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

6 files changed, 77 insertions, 63 deletions

diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index 573ac2dd32..700ac67349 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -153,7 +153,7 @@ GEXTEND Gram
     [ [ c = operconstr -> c ] ]
   ;
   constr:
-    [ [ c = operconstr LEVEL "9" -> c ] ]
+    [ [ c = operconstr LEVEL "9L" -> c ] ]
   ;
   tuple_constr:
     [ 
@@ -174,14 +174,12 @@ GEXTEND Gram
       [ "-"; c = operconstr -> CNotation(loc,"- _",[c]) ]
     | "10L" LEFTA
       [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,(None,f),args)
-      | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(None,f),args)
-      |	c=operconstr; ".("; f=global; args1=LIST0 appl_arg; ")";
-          args2=LIST0 appl_arg -> 
-	    CApp(loc,(Some (List.length args1+1),CRef f),args1@(c,None)::args2)
-      | c=operconstr; ".("; "@"; f=global; args1=LIST0 NEXT; ")";
-          args2=LIST0 NEXT -> 
-	    CAppExpl(loc,(Some (List.length args1+1),f),args1@c::args2) ]
-    | "9" [ ]
+      | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(None,f),args) ]
+    | "9L" LEFTA
+      [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" ->
+	CApp(loc,(Some (List.length args+1),CRef f),args@[c,None])
+      | c=operconstr; ".("; "@"; f=global; args=LIST0 NEXT; ")" ->
+        CAppExpl(loc,(Some (List.length args+1),f),args@[c]) ]
     | "1L" LEFTA
       [ c=operconstr; "%"; key=IDENT -> CDelimiters (loc,key,c) ]
     | "0"
@@ -212,8 +210,8 @@ GEXTEND Gram
       | c=fix_constr -> c ] ]
   ;
   appl_arg:
-    [ [ "@"; n=INT; ":="; c=operconstr LEVEL "9" -> (c,Some(int_of_string n))
-      | c=operconstr LEVEL "9" -> (c,None) ] ]
+    [ [ "@"; n=INT; ":="; c=constr -> (c,Some(int_of_string n))
+      | c=constr -> (c,None) ] ]
   ;
   atomic_constr:
     [ [ g=global -> CRef g
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index 54c671ed69..e4810cda06 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -111,17 +111,17 @@ GEXTEND Gram
   constrarg:
     [ [ IDENT "inst"; id = identref; "["; c = Constr.lconstr; "]" ->
         ConstrContext (id, c)
-      | IDENT "eval"; rtc = Tactic.red_expr; "in"; c = Constr.lconstr ->
+      | IDENT "eval"; rtc = Tactic.red_expr; "in"; c = Constr.constr ->
         ConstrEval (rtc,c) 
-      | IDENT "check"; c = Constr.lconstr -> ConstrTypeOf c
+      | IDENT "check"; c = Constr.constr -> ConstrTypeOf c
       | c = Constr.lconstr -> ConstrTerm c ] ]
   ;
   castedopenconstr:
-    [ [ c = lconstr -> c ] ]
+    [ [ c = constr -> c ] ]
   ;
   induction_arg:
     [ [ n = natural -> ElimOnAnonHyp n
-      | c = lconstr -> induction_arg_of_constr c
+      | c = constr -> induction_arg_of_constr c
     ] ]
   ;
   quantified_hypothesis:
@@ -251,14 +251,14 @@ GEXTEND Gram
       | IDENT "intro" -> TacIntroMove (None, None)
 
       | IDENT "assumption" -> TacAssumption
-      | IDENT "exact"; c = lconstr -> TacExact c
+      | IDENT "exact"; c = constr -> TacExact c
 
       | IDENT "apply"; cl = constr_with_bindings -> TacApply cl
       | IDENT "elim"; cl = constr_with_bindings; el = OPT eliminator ->
           TacElim (cl,el)
-      | IDENT "elimtype"; c = lconstr -> TacElimType c
+      | IDENT "elimtype"; c = constr -> TacElimType c
       | IDENT "case"; cl = constr_with_bindings -> TacCase cl
-      | IDENT "casetype"; c = lconstr -> TacCaseType c
+      | IDENT "casetype"; c = constr -> TacCaseType c
       | "fix"; n = natural -> TacFix (None,n)
       | "fix"; id = base_ident; n = natural -> TacFix (Some id,n)
       | "fix"; id = base_ident; n = natural; "with"; fd = LIST0 fixdecl ->
@@ -268,26 +268,25 @@ GEXTEND Gram
       | "cofix"; id = base_ident; "with"; fd = LIST0 cofixdecl ->
 	  TacMutualCofix (id,fd)
 
-      | IDENT "cut"; c = lconstr -> TacCut c
-      | IDENT "assert"; c = lconstr ->
-          (match c with
-              Topconstr.CCast(_,c,t) -> TacTrueCut (Some (coerce_to_id c),t)
-            | _ -> TacTrueCut (None,c))
-      | IDENT "assert"; c = lconstr; ":="; b = lconstr ->
+      | IDENT "cut"; c = constr -> TacCut c
+      | IDENT "assert"; c = constr -> TacTrueCut (None,c)
+      | IDENT "assert"; c = constr; ":"; t = lconstr ->
+          TacTrueCut (Some (coerce_to_id c),t)
+      | IDENT "assert"; c = constr; ":="; b = lconstr ->
           TacForward (false,Names.Name (coerce_to_id c),b)
-      | IDENT "pose"; c = lconstr; ":="; b = lconstr ->
+      | IDENT "pose"; c = constr; ":="; b = lconstr ->
 	  TacForward (true,Names.Name (coerce_to_id c),b)
-      | IDENT "pose"; b = lconstr -> TacForward (true,Names.Anonymous,b)
+      | IDENT "pose"; b = constr -> TacForward (true,Names.Anonymous,b)
       | IDENT "generalize"; lc = LIST1 constr -> TacGeneralize lc
-      | IDENT "generalize"; IDENT "dependent"; c = lconstr ->
+      | IDENT "generalize"; IDENT "dependent"; c = constr ->
           TacGeneralizeDep c
       | IDENT "lettac"; id = base_ident; ":="; c = lconstr; p = clause_pattern
         -> TacLetTac (id,c,p)
-      | IDENT "instantiate"; n = natural; c = lconstr -> TacInstantiate (n,c)
+      | IDENT "instantiate"; n = natural; c = constr -> TacInstantiate (n,c)
 
       | IDENT "specialize"; n = OPT natural; lcb = constr_with_bindings ->
 	  TacSpecialize (n,lcb)
-      | IDENT "lapply"; c = lconstr -> TacLApply c
+      | IDENT "lapply"; c = constr -> TacLApply c
 
       (* Derived basic tactics *)
       | IDENT "oldinduction"; h = quantified_hypothesis -> TacOldInduction h
@@ -298,9 +297,9 @@ GEXTEND Gram
       | IDENT "olddestruct"; h = quantified_hypothesis -> TacOldDestruct h
       | IDENT "destruct"; c = induction_arg; el = OPT eliminator; 
           ids = with_names -> TacNewDestruct (c,el,ids)
-      | IDENT "decompose"; IDENT "record" ; c = lconstr -> TacDecomposeAnd c
-      | IDENT "decompose"; IDENT "sum"; c = lconstr -> TacDecomposeOr c
-      | IDENT "decompose"; "["; l = LIST1 global; "]"; c = lconstr
+      | IDENT "decompose"; IDENT "record" ; c = constr -> TacDecomposeAnd c
+      | IDENT "decompose"; IDENT "sum"; c = constr -> TacDecomposeOr c
+      | IDENT "decompose"; "["; l = LIST1 global; "]"; c = constr
         -> TacDecompose (l,c)
 
       (* Automation tactic *)
@@ -337,7 +336,7 @@ GEXTEND Gram
       | IDENT "reflexivity" -> TacReflexivity
       | IDENT "symmetry"; ido = OPT [ "in"; id = id_or_meta -> id ] -> 
 	  TacSymmetry ido
-      | IDENT "transitivity"; c = lconstr -> TacTransitivity c
+      | IDENT "transitivity"; c = constr -> TacTransitivity c
 
       (* Conversion *)
       | r = red_tactic; cl = clause -> TacReduce (r, cl)
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index fb952a4e9a..6b11d5c985 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -505,7 +505,7 @@ GEXTEND Gram
 	  VernacRemoveLoadPath dir
 
       (* Type-Checking (pas dans le refman) *)
-      | "Type"; c = lconstr -> VernacGlobalCheck c
+      | "Type"; c = constr -> VernacGlobalCheck c
 
       (* Printing (careful factorization of entries) *)
       | IDENT "Print"; p = printable -> VernacPrint p
@@ -577,9 +577,9 @@ GEXTEND Gram
 	  VernacRemoveOption (PrimaryTable table, v) ] ]
   ;
   check_command: (* TODO: rapprocher Eval et Check *)
-    [ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = lconstr ->
+    [ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = constr ->
           fun g -> VernacCheckMayEval (Some r, g, c)
-      | IDENT "Check"; c = lconstr ->
+      | IDENT "Check"; c = constr ->
 	  fun g -> VernacCheckMayEval (None, g, c) ] ]
   ;
   printable:
@@ -701,10 +701,16 @@ GEXTEND Gram
 
      | IDENT "Grammar"; u = univ;
          tl = LIST1 grammar_entry SEP "with" -> 
+	   failwith "Grammar for constr not supported in v8; use Notation"
+(*
 	   VernacGrammar (rename_command_entry u,tl)
+*)
 
      | IDENT "Syntax"; u = univ; el = LIST1 syntax_entry SEP "," ->
+	   failwith "Syntax not supported in v8; use Notation"
+(*
          VernacSyntax (u,el)
+*)
 
      | IDENT "Uninterpreted"; IDENT "Notation"; local = locality; s = STRING; 
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]
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"