Suppression code pour hints nommés à la V7 (voire à la V6...)

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

2 files changed, 17 insertions, 25 deletions

diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 80dcf23e3..5d392846d 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -34,7 +34,7 @@ GEXTEND Gram
     | ":"; l = LIST1 IDENT -> l ] ]
   ;
   command:
-    [ [ IDENT "Goal"; c = Constr.lconstr -> VernacGoal c
+    [ [ IDENT "Goal"; c = lconstr -> VernacGoal c
       | IDENT "Proof" -> VernacProof (Tacexpr.TacId [])
       | IDENT "Proof"; "with"; ta = tactic -> VernacProof ta
       | IDENT "Abort" -> VernacAbort None
@@ -56,7 +56,7 @@ GEXTEND Gram
       | IDENT "Resume" -> VernacResume None
       | IDENT "Resume"; id = identref -> VernacResume (Some id)
       | IDENT "Restart" -> VernacRestart
-      | IDENT "Proof"; c = Constr.lconstr -> VernacExactProof c
+      | IDENT "Proof"; c = lconstr -> VernacExactProof c
       | IDENT "Undo" -> VernacUndo 1
       | IDENT "Undo"; n = natural -> VernacUndo n
       | IDENT "Focus" -> VernacFocus None
@@ -91,7 +91,7 @@ GEXTEND Gram
 	  
 
 (*This entry is not commented, only for debug*)
-      | IDENT "PrintConstr"; c = Constr.constr -> 
+      | IDENT "PrintConstr"; c = constr -> 
 	  VernacExtend ("PrintConstr",
 	    [Genarg.in_gen Genarg.rawwit_constr c])
       ] ];
@@ -100,22 +100,18 @@ GEXTEND Gram
     [ [ IDENT "Local" -> true | -> false ] ]
   ;
   hint:
-    [ [ 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 ; "=>";
+    [ [ IDENT "Resolve"; lc = LIST1 constr -> HintsResolve lc
+      | IDENT "Immediate"; lc = LIST1 constr -> HintsImmediate lc
+      | IDENT "Unfold"; lqid = LIST1 global -> HintsUnfold lqid
+      | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc
+      | IDENT "Extern"; n = natural; c = constr_pattern ; "=>";
           tac = tactic ->
-	  HintsExtern (None,n,c,tac)
-      | IDENT"Destruct"; 
+	  HintsExtern (n,c,tac)
+      | IDENT "Destruct"; 
           id = ident; ":=";
           pri = natural;
           dloc = destruct_location;
-          hyptyp = Constr.constr_pattern;
+          hyptyp = constr_pattern;
           "=>"; tac = tactic ->
             HintsDestruct(id,pri,dloc,hyptyp,tac) ] ]
     ;
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 2444b1be9..378417a12 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -184,18 +184,14 @@ let pr_hints local db h pr_c pr_pat =
   let pph =
     match h with
     | HintsResolve l ->
-        str "Resolve " ++
-        prlist_with_sep sep pr_c (List.map snd l)
+        str "Resolve " ++ prlist_with_sep sep pr_c l
     | HintsImmediate l ->
-        str"Immediate" ++ spc() ++
-        prlist_with_sep sep pr_c (List.map snd l)
+        str"Immediate" ++ spc() ++ prlist_with_sep sep pr_c l
     | HintsUnfold l ->
-        str "Unfold " ++
-	prlist_with_sep sep pr_reference (List.map snd l)
-    | HintsConstructors (n,c) ->
-        str"Constructors" ++ spc() ++
-        prlist_with_sep spc pr_reference c
-    | HintsExtern (name,n,c,tac) ->
+        str "Unfold " ++ prlist_with_sep sep pr_reference l
+    | HintsConstructors c ->
+        str"Constructors" ++ spc() ++ prlist_with_sep spc pr_reference c
+    | HintsExtern (n,c,tac) ->
         str "Extern" ++ spc() ++ int n ++ spc() ++ pr_pat c ++ str" =>" ++
         spc() ++ pr_raw_tactic tac
     | HintsDestruct(name,i,loc,c,tac) ->