Légère amélioration des messages d'erreur des with-bindings et des Rewrite

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

3 files changed, 11 insertions, 27 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 5cfc324eb..c7f8217d1 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -47,28 +47,9 @@ let local_compute =
     Qast.Node ("FIota", []);
     Qast.Node ("FZeta", [])]
 
-(*
-  let
-    {rBeta = b; rIota = i; rZeta = z; rDelta = d; rConst = l} = make_red_flag s
-  in
-  let quotify_ident id =
-    Qast.Apply ("Names.id_of_string", [Qast.Str (Names.string_of_id id)])
-  in
-  let quotify_path sp =
-    let dir, id = Names.repr_path sp in
-    let l = Names.repr_dirpath dir in
-    Qast.Apply ("Names.make_path",
-      [Qast.Apply ("Names.make_dirpath",
-        [Qast.List (List.map quotify_ident l)]);
-      quotify_ident id]) in
-  Qast.Record 
-    ["rBeta",Qast.Bool b; "rIota",Qast.Bool i;
-     "rZeta",Qast.Bool z; "rDelta",Qast.Bool d;
-     "rConst",Qast.List (List.map quotify_path l)]
-*)
 ifdef Quotify then open Q
 
-(* Please leave several GEXTEND for modular compilation under PowerPC *)
+let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2)
 
 (* Auxiliary grammar rules *)
 
@@ -169,14 +150,15 @@ GEXTEND Gram
       ] ]
   ;
   simple_binding:
-    [ [ id = base_ident; ":="; c = constr -> (NamedHyp id, c)
-      | n = natural; ":="; c = constr -> (AnonHyp n, c) ] ]
+    [ [ id = base_ident; ":="; c = constr -> (loc, NamedHyp id, c)
+      | n = natural; ":="; c = constr -> (loc, AnonHyp n, c) ] ]
   ;
   binding_list:
     [ [ c1 = constr; ":="; c2 = constr; bl = LIST0 simple_binding ->
-          ExplicitBindings ((NamedHyp (coerce_to_id c1), c2) :: bl)
+          ExplicitBindings
+            ((join_to_constr loc c2,NamedHyp (coerce_to_id c1), c2) :: bl)
       | n = natural; ":="; c = constr; bl = LIST0 simple_binding ->
-	  ExplicitBindings ((AnonHyp n, c) :: bl)
+	  ExplicitBindings ((join_to_constr loc c,AnonHyp n, c) :: bl)
       | c1 = constr; bl = LIST0 constr ->
 	  ImplicitBindings (c1 :: bl) ] ]
   ;
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 6c45c9e70..c44881614 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -75,8 +75,8 @@ let pr_quantified_hypothesis = function
 let pr_quantified_hypothesis_arg h = spc () ++ pr_quantified_hypothesis h
 
 let pr_binding prc = function
-  | NamedHyp id, c -> hov 1 (pr_id id ++ str ":=" ++ cut () ++ prc c)
-  | AnonHyp n, c -> hov 1 (int n ++ str ":=" ++ cut () ++ prc c)
+  | loc, NamedHyp id, c -> hov 1 (pr_id id ++ str ":=" ++ cut () ++ prc c)
+  | loc, AnonHyp n, c -> hov 1 (int n ++ str ":=" ++ cut () ++ prc c)
 
 let pr_bindings prc = function
   | ImplicitBindings l ->
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index bc8128fd8..1f352f6af 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -159,6 +159,8 @@ let mlexpr_of_quantified_hypothesis = function
 
 let mlexpr_of_located f (loc,x) = <:expr< ($dloc$, $f x$) >>
 
+let mlexpr_of_loc loc = <:expr< $dloc$ >>
+
 let mlexpr_of_hyp_location = function
   | Tacexpr.InHyp id ->
       <:expr< Tacexpr.InHyp $mlexpr_of_or_metaid (mlexpr_of_located mlexpr_of_ident) id$ >>
@@ -268,7 +270,7 @@ let rec mlexpr_of_may_eval f = function
 
 let mlexpr_of_binding_kind = function
   | Rawterm.ExplicitBindings l ->
-      let l = mlexpr_of_list (mlexpr_of_pair mlexpr_of_quantified_hypothesis mlexpr_of_constr) l in
+      let l = mlexpr_of_list (mlexpr_of_triple mlexpr_of_loc mlexpr_of_quantified_hypothesis mlexpr_of_constr) l in
       <:expr< Rawterm.ExplicitBindings $l$ >>
   | Rawterm.ImplicitBindings l -> 
       let l = mlexpr_of_list mlexpr_of_constr l in