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, 39 insertions, 36 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 | -> [] ]