adds the possibility to have terms (and not just identifiers) as hints

Adds the 'Reserved Notation' command


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

1 files changed, 27 insertions, 26 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 0a9dffb9d..ccc1c8c60 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1610,34 +1610,28 @@ let rec xlate_vernac =
 		      CT_id_ne_list(n1, names), dblist)
 	| HintsExtern (None, n, c, t) ->
 	    CT_hint_extern(CT_int n, xlate_formula c, xlate_tactic t, dblist)
-        | HintsResolve l -> 
-	 let l = 
-	   List.map 
-	     (function (None,CRef r) -> r 
-		| _ -> xlate_error "obsolete Hint Resolve not supported") l in
-	 let n1, names = match List.map tac_qualid_to_ct_ID l with
-	     n1 :: names -> n1, names
-	   | _  -> failwith "" in
-	   if local then
-             CT_local_hints(CT_ident "Resolve",
-			    CT_id_ne_list(n1, names), dblist)
-	   else
-             CT_hints(CT_ident "Resolve", CT_id_ne_list(n1, names), dblist)
-        | HintsImmediate l -> 
-	    let l =
+        | HintsResolve l | HintsImmediate l -> 
+	    let l = 
 	      List.map 
-		(function (None,CRef r) -> r 
-		   | _ ->
-		       xlate_error "obsolete Hint Immediate not supported") l
-	    in
-	 let n1, names = match List.map tac_qualid_to_ct_ID l with
-	     n1 :: names -> n1, names
+	     	(function (None, f) -> xlate_formula f
+		   | _ -> 
+		       xlate_error "obsolete Hint Resolve not supported") l in
+	 let f1, formulas = match l  with
+	     a :: tl -> a, tl
 	   | _  -> failwith "" in
+	 let l' = CT_formula_ne_list(f1, formulas) in
 	   if local then
-             CT_local_hints(CT_ident "Immediate",
-			    CT_id_ne_list(n1, names), dblist)
+             (match h with 
+		  HintsResolve _ ->
+		    CT_local_hints_resolve(l', dblist)
+	       	| HintsImmediate _ ->
+		    CT_local_hints_immediate(l', dblist)
+	       	| _ -> assert false)
 	   else
-             CT_hints(CT_ident "Immediate", CT_id_ne_list(n1, names), dblist)
+	     (match h with
+		  HintsResolve _ -> CT_hints_resolve(l', dblist)
+		| HintsImmediate _ -> CT_hints_immediate(l', dblist)
+		| _ -> assert false)
         | HintsUnfold l -> 
 	 let l = List.map
 	   (function (None,ref) -> loc_qualid_to_ct_ID ref |
@@ -1921,8 +1915,15 @@ let rec xlate_vernac =
        else
 	 CT_define_notation(translated_s, formula, 
 			    translated_modif_list, translated_scope)
-   | VernacSyntaxExtension _ -> xlate_error "Syntax Extension not implemented"
-
+   | VernacSyntaxExtension(b,Some(s,modif_list), None) -> 
+       let translated_s = CT_string s in
+       let translated_modif_list = 
+	 CT_modifier_list(List.map xlate_syntax_modifier modif_list) in
+       if b then
+	 CT_local_reserve_notation(translated_s, translated_modif_list)
+       else
+	 CT_reserve_notation(translated_s, translated_modif_list)
+   | VernacSyntaxExtension(_, _, _) -> assert false
    | VernacInfix (b,(str,modl),id,_, opt_scope) ->
        let id1 = loc_qualid_to_ct_ID id in
        let modl1 = CT_modifier_list(List.map xlate_syntax_modifier modl) in