reorganisation des niveaux (ex: = est a 70)

Hint Destruct: syntaxe similaire aux autres hints...


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

6 files changed, 35 insertions, 38 deletions

diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 3337fbc0b..fad041f20 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -220,7 +220,10 @@ END
 (* Grammar extensions *)
 
 (* automatic translation of levels *)
-let adapt_level n = n*10
+let adapt_level n =
+  if n >= 10 then n*10 else
+    [| 0; 20; 30; 40; 50; 70; 80; 85; 90; 95; 100|].(n)
+
 let map_modl = function
   | SetItemLevel(ids,NumLevel n) -> SetItemLevel(ids,NumLevel (adapt_level n))
   | SetLevel n -> SetLevel(adapt_level n)
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index d11d982ff..d5d1db939 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -174,7 +174,8 @@ GEXTEND Gram
     | "100" RIGHTA
       [ c1 = operconstr; ":"; c2 = binder_constr -> CCast(loc,c1,c2)
       | c1 = operconstr; ":"; c2 = operconstr    -> CCast(loc,c1,c2) ]
-    | "80" RIGHTA
+    | "99" RIGHTA [ ]
+    | "90" RIGHTA
       [ c1 = operconstr; "->"; c2 = binder_constr -> CArrow(loc,c1,c2)
       | c1 = operconstr; "->"; c2 = operconstr    -> CArrow(loc,c1,c2) ]
     | "10" LEFTA
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 1cc9f038f..c462c3bdc 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -92,7 +92,7 @@ GEXTEND Gram
           hyptyp = Constr.constr_pattern;
           pri = natural;
           "["; tac = tactic; "]" -> 
-	    VernacHintDestruct (local,id,dloc,hyptyp,pri,tac)
+	    VernacHints(local,[],HintsDestruct (id,pri,dloc,hyptyp,tac))
 
       | IDENT "Hint"; local = locality; hintname = base_ident; 
 	  dbnames = opt_hintbases; ":="; h = hint
@@ -115,9 +115,10 @@ GEXTEND Gram
     [ [ IDENT "Resolve"; c = Constr.constr -> fun name -> HintsResolve [Some name, c]
       | IDENT "Immediate"; c = Constr.constr -> fun name -> HintsImmediate [Some name, c]
       | IDENT "Unfold"; qid = global -> fun name -> HintsUnfold [Some name,qid]
-      | IDENT "Constructors"; c = global -> fun n -> HintsConstructors (n,c)
+      | IDENT "Constructors"; c = global -> fun n ->
+          HintsConstructors (Some n,[c])
       | IDENT "Extern"; n = natural; c = Constr.constr ; tac = tactic ->
-	  fun name -> HintsExtern (name,n,c,tac) ] ]
+	  fun name -> HintsExtern (Some name,n,c,tac) ] ]
   ;
   hints:
     [ [ IDENT "Resolve"; l = LIST1 global; dbnames = opt_hintbases ->
diff --git a/parsing/g_proofsnew.ml4 b/parsing/g_proofsnew.ml4
index eb1b3e466..7d75cf4cb 100644
--- a/parsing/g_proofsnew.ml4
+++ b/parsing/g_proofsnew.ml4
@@ -85,21 +85,8 @@ GEXTEND Gram
       | IDENT "Go"; IDENT "next" -> VernacGo GoNext
       | IDENT "Guarded" -> VernacCheckGuard
 (* Hints for Auto and EAuto *)
-
-      | IDENT "HintDestruct"; 
-	  local = locality;
-          dloc = destruct_location;
-          id  = base_ident;
-          hyptyp = Constr.constr_pattern;
-          pri = natural;
-          "["; tac = tactic; "]" -> 
-	    VernacHintDestruct (local,id,dloc,hyptyp,pri,tac)
-
-      | IDENT "Hint"; local = locality; hintname = base_ident; 
-	  dbnames = opt_hintbases; ":="; h = hint ->
-            VernacHints (local,dbnames, h hintname)
-	  
-      | IDENT "Hints"; local = locality; (dbnames,h) = hints ->
+      | IDENT "Hint"; local = locality; h = hint;
+        dbnames = opt_hintbases ->
 	  VernacHints (local,dbnames, h)
 	  
 
@@ -113,20 +100,24 @@ GEXTEND Gram
     [ [ IDENT "Local" -> true | -> false ] ]
   ;
   hint:
-    [ [ IDENT "Resolve"; c = Constr.constr -> fun name -> HintsResolve [Some name, c]
-      | IDENT "Immediate"; c = Constr.constr -> fun name -> HintsImmediate [Some name, c]
-      | IDENT "Unfold"; qid = global -> fun name -> HintsUnfold [Some name,qid]
-      | IDENT "Constructors"; c = global -> fun n -> HintsConstructors (n,c)
-      | IDENT "Extern"; n = natural; c = Constr.constr ; tac = tactic ->
-	  fun name -> HintsExtern (name,n,c,tac) ] ]
-  ;
-  hints:
-    [ [ IDENT "Resolve"; l = LIST1 global; dbnames = opt_hintbases ->
-         (dbnames, HintsResolve (List.map (fun qid -> (None, CRef qid)) l))
-      | IDENT "Immediate"; l = LIST1 global; dbnames = opt_hintbases ->
-        (dbnames, HintsImmediate (List.map (fun qid -> (None, CRef qid)) l))
-      | IDENT "Unfold"; l = LIST1 global; dbnames = opt_hintbases ->
-        (dbnames, HintsUnfold (List.map (fun qid -> (None,qid)) l)) ] ]
+    [ [ IDENT "Resolve"; lc = LIST1 Constr.constr ->
+          HintsResolve (List.map (fun c -> (None, c)) lc)
+      | IDENT "Immediate"; lc = LIST1 Constr.constr ->
+          HintsImmediate (List.map (fun c -> (None,c)) lc)
+      | IDENT "Unfold"; lqid = LIST1 global ->
+          HintsUnfold (List.map (fun g -> (None,g)) lqid)
+      | IDENT "Constructors"; lc = LIST1 global ->
+          HintsConstructors (None,lc)
+      | IDENT "Extern"; n = natural; c = Constr.constr_pattern ; "=>";
+          tac = tactic ->
+	  HintsExtern (None,n,c,tac)
+      | IDENT"Destruct"; 
+          id = base_ident; ":=";
+          pri = natural;
+          dloc = destruct_location;
+          hyptyp = Constr.constr_pattern;
+          "=>"; tac = tactic ->
+            HintsDestruct(id,pri,dloc,hyptyp,tac) ] ]
     ;
   constr_body:
     [ [ ":="; c = lconstr -> c
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 90ef93d89..9e718cfd6 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -499,7 +499,7 @@ GEXTEND Gram
 	  VernacRemoveLoadPath dir
 
       (* Type-Checking (pas dans le refman) *)
-      | "Type"; c = constr -> VernacGlobalCheck c
+      | "Type"; c = lconstr -> VernacGlobalCheck c
 
       (* Printing (careful factorization of entries) *)
       | IDENT "Print"; p = printable -> VernacPrint p
@@ -574,9 +574,9 @@ GEXTEND Gram
 	  VernacRemoveOption (PrimaryTable table, v) ] ]
   ;
   check_command: (* TODO: rapprocher Eval et Check *)
-    [ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = constr ->
+    [ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = lconstr ->
           fun g -> VernacCheckMayEval (Some r, g, c)
-      | IDENT "Check"; c = constr ->
+      | IDENT "Check"; c = lconstr ->
 	  fun g -> VernacCheckMayEval (None, g, c) ] ]
   ;
   printable:
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 8d1d189ba..152141bfa 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -545,7 +545,8 @@ let default_levels_v7 =
 let default_levels_v8 =
   [200,Gramext.RightA;
    100,Gramext.RightA;
-   80,Gramext.RightA;
+   99,Gramext.RightA;
+   90,Gramext.RightA;
    10,Gramext.LeftA;
    9,Gramext.RightA;
    1,Gramext.LeftA;