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

5 files changed, 23 insertions, 22 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 84c07dc71c..947ead355c 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -255,7 +255,7 @@ and ct_FORMULA_OR_INT =
 and ct_GRAMMAR =
     CT_grammar_none
 and ct_HINT_EXPRESSION =
-    CT_constructors of ct_ID
+    CT_constructors of ct_ID_LIST
   | CT_extern of ct_INT * ct_FORMULA * ct_TACTIC_COM
   | CT_immediate of ct_FORMULA
   | CT_resolve of ct_FORMULA
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 677f7edc95..760c2286a4 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -655,7 +655,7 @@ and fGRAMMAR = function
 | CT_grammar_none -> fNODE "grammar_none" 0
 and fHINT_EXPRESSION = function
 | CT_constructors(x1) ->
-   fID x1;
+   fID_LIST x1;
    fNODE "constructors" 1
 | CT_extern(x1, x2, x3) ->
    fINT x1;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 6fd12a0107..c3355b61bb 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1366,13 +1366,13 @@ let xlate_vernac =
 	| HintsUnfold [Some id_name, q] -> (* = Old HintUnfold *)
 	    CT_hint(xlate_ident id_name, dblist,
               CT_unfold_hint (loc_qualid_to_ct_ID q))
-	| HintsConstructors (id_name, q) ->
+	| HintsConstructors (Some id_name, ql) ->
 	    CT_hint(xlate_ident id_name, dblist,
-              CT_constructors (loc_qualid_to_ct_ID q))
-	| HintsExtern (id_name, n, c, t) ->
+              CT_constructors (CT_id_list(List.map loc_qualid_to_ct_ID ql)))
+	| HintsExtern (Some id_name, n, c, t) ->
 	    CT_hint(xlate_ident id_name, dblist,
               CT_extern(CT_int n, xlate_formula c, xlate_tactic t))
-     | HintsResolve l -> (* = Old HintsResolve *)
+        | HintsResolve l -> (* = Old HintsResolve *)
 	 let l = List.map (function (None,CRef r) -> r | _ -> failwith "") l in
 	 let n1, names = match List.map tac_qualid_to_ct_ID l with
 	     n1 :: names -> n1, names
@@ -1380,7 +1380,7 @@ let xlate_vernac =
          CT_hints(CT_ident "Resolve",
                   CT_id_ne_list(n1, names),
 		  dblist)
-     | HintsImmediate l -> (* = Old HintsImmediate *)
+        | HintsImmediate l -> (* = Old HintsImmediate *)
 	 let l = List.map (function (None,CRef r) -> r | _ -> failwith "") l in
 	 let n1, names = match List.map tac_qualid_to_ct_ID l with
 	     n1 :: names -> n1, names
@@ -1388,7 +1388,7 @@ let xlate_vernac =
         CT_hints(CT_ident "Immediate", 
                  CT_id_ne_list(n1, names),
                  dblist)
-     | HintsUnfold l ->  (* = Old HintsUnfold *)
+        | HintsUnfold l ->  (* = Old HintsUnfold *)
 	 let l = List.map
 	   (function
 	       (None,ref) -> loc_qualid_to_ct_ID ref
@@ -1398,7 +1398,8 @@ let xlate_vernac =
 	   | _  -> failwith "" in
         CT_hints(CT_ident "Unfold", 
                  CT_id_ne_list(n1, names),
-                 dblist))
+                 dblist)
+        | _ -> xlate_error"TODO: Hint")
   | VernacEndProof (Proved (true,None)) ->
       CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Theorem"), ctv_ID_OPT_NONE)
   | VernacEndProof (Proved (false,None)) ->
@@ -1676,7 +1677,7 @@ let xlate_vernac =
   | (VernacGlobalCheck _|VernacPrintOption _|
      VernacMemOption (_, _)|VernacRemoveOption (_, _)|VernacAddOption (_, _)|
      VernacSetOption (_, _)|VernacUnsetOption _|
-     VernacHintDestruct (_, _, _, _, _, _)|VernacBack _|VernacRestoreState _|
+     VernacBack _|VernacRestoreState _|
      VernacWriteState _|VernacSolveExistential (_, _)|VernacCanonical _|
      VernacImport (_, _)|VernacExactProof _|VernacDistfix _|
      VernacTacticGrammar _|VernacVar _|VernacTime _|VernacProof _)
diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v
index 3a3fb0640b..55ad8023f3 100644
--- a/contrib/ring/Ring_theory.v
+++ b/contrib/ring/Ring_theory.v
@@ -25,8 +25,8 @@ Variable Azero : A.
   is a good choice. The proof of A_eq_prop is in this case easy. *)
 Variable Aeq : A -> A -> bool.
 
-Infix 4 "+" Aplus V8only 40 (left associativity).
-Infix 4 "*" Amult V8only 30 (left associativity).
+Infix 4 "+" Aplus V8only 50 (left associativity).
+Infix 4 "*" Amult V8only 40 (left associativity).
 Notation "0" := Azero.
 Notation "1" := Aone.
 
@@ -146,16 +146,16 @@ Variable Azero : A.
 Variable Aopp : A -> A.
 Variable Aeq : A -> A -> bool.
 
-Infix 4 "+" Aplus V8only 40 (left associativity).
-Infix 4 "*" Amult V8only 30 (left associativity).
+Infix 4 "+" Aplus V8only 50 (left associativity).
+Infix 4 "*" Amult V8only 40 (left associativity).
 Notation "0" := Azero.
 Notation "1" := Aone.
 Notation "- 0" := (Aopp Azero) (at level 0)
-  V8only (at level 40, left associativity).
+  V8only (at level 50, left associativity).
 Notation "- 1" := (Aopp Aone) (at level 0)
-  V8only (at level 40, left associativity).
+  V8only (at level 50, left associativity).
 Notation "- x" := (Aopp x) (at level 0)
-  V8only (at level 40, left associativity).
+  V8only (at level 50, left associativity).
 
 Record Ring_Theory : Prop :=
 { Th_plus_sym  : (n,m:A) n + m == m + n;
diff --git a/contrib/ring/Setoid_ring_theory.v b/contrib/ring/Setoid_ring_theory.v
index 8b9ae52f0f..c97536846b 100644
--- a/contrib/ring/Setoid_ring_theory.v
+++ b/contrib/ring/Setoid_ring_theory.v
@@ -31,16 +31,16 @@ Variable Azero : A.
 Variable Aopp : A -> A.
 Variable Aeq : A -> A -> bool.
 
-Infix 4 "+" Aplus V8only 40 (left associativity).
-Infix 4 "*" Amult V8only 30 (left associativity).
+Infix 4 "+" Aplus V8only 50 (left associativity).
+Infix 4 "*" Amult V8only 40 (left associativity).
 Notation "0" := Azero.
 Notation "1" := Aone.
 Notation "- 0" := (Aopp Azero) (at level 0)
-  V8only (at level 40, left associativity).
+  V8only (at level 50, left associativity).
 Notation "- 1" := (Aopp Aone) (at level 0)
-  V8only (at level 40, left associativity).
+  V8only (at level 50, left associativity).
 Notation "- x" := (Aopp x) (at level 0)
-  V8only (at level 40, left associativity).
+  V8only (at level 50, left associativity).
 
 Variable plus_morph : (a,a0,a1,a2:A) a == a0 -> a1 == a2 -> a+a1 == a0+a2.
 Variable mult_morph : (a,a0,a1,a2:A) a == a0 -> a1 == a2 -> a*a1 == a0*a2.