meilleure presentation des commentaires du traducteur

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

1 files changed, 3 insertions, 2 deletions

diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index db2617da33..77d516a136 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -56,11 +56,12 @@ let tuple_n n =
       (fun i -> 
 	 let id = make_ident ("proj_" ^ string_of_int n ^ "_") (Some i) in
 	 let id' = make_ident "T" (Some i) in
-	 (false, Vernacexpr.AssumExpr (id, mkIdentC id')))
+	 (false, Vernacexpr.AssumExpr ((dummy_loc,id), mkIdentC id')))
       l1n 
   in
   let cons = make_ident "Build_tuple_" (Some n) in
-  Record.definition_structure ((false, id), params, fields, cons, mk_Set)
+  Record.definition_structure
+    ((false, (dummy_loc,id)), params, fields, cons, mk_Set)
 
 (*s [(sig_n n)] generates the inductive
     \begin{verbatim}