3 files changed, 8 insertions, 11 deletions
diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index ecc17253a1..d13be77200 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -48,7 +48,7 @@ let tuple_n n =
       (fun i -> 
 	 let id = id_of_string 
 		    ("proj_" ^ string_of_int n ^ "_" ^ string_of_int i) in
-	 (false, (id, true, Ast.nvar ("T" ^ string_of_int i))))
+	 (false, (id, true, Ast.nvar (id_of_string ("T" ^ string_of_int i)))))
       l1n 
   in
   let cons = id_of_string ("Build_tuple_" ^ string_of_int n) in
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index d6a15959b2..c885242bda 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -120,23 +120,19 @@ let subst_in_constr alist =
   replace_vars alist'
 
 let subst_in_ast alist ast =
-  let alist' = 
-    List.map (fun (id,id') -> (string_of_id id,string_of_id id')) alist in
   let rec subst = function
-      Nvar(l,s) -> Nvar(l,try List.assoc s alist' with Not_found -> s)
+      Nvar(l,s) -> Nvar(l,try List.assoc s alist with Not_found -> s)
     | Node(l,s,args) -> Node(l,s,List.map subst args)
-    | Slam(l,so,a) -> Slam(l,so,subst a) (* TODO:enlever so de alist' ? *)
+    | Slam(l,so,a) -> Slam(l,so,subst a) (* TODO:enlever so de alist ? *)
     | x -> x
   in
     subst ast
 
 let subst_ast_in_ast alist ast =
-  let alist' = 
-    List.map (fun (id,a) -> (string_of_id id,a)) alist in
   let rec subst = function
-      Nvar(l,s) as x -> (try List.assoc s alist' with Not_found -> x)
+      Nvar(l,s) as x -> (try List.assoc s alist with Not_found -> x)
     | Node(l,s,args) -> Node(l,s,List.map subst args)
-    | Slam(l,so,a) -> Slam(l,so,subst a) (* TODO:enlever so de alist' ? *)
+    | Slam(l,so,a) -> Slam(l,so,subst a) (* TODO:enlever so de alist ? *)
     | x -> x
   in
     subst ast
@@ -146,7 +142,8 @@ let real_subst_in_constr = replace_vars
 
 (* Coq constants *)
 
-let coq_constant d s = make_path ("Coq" :: d) (id_of_string s) CCI
+let coq_constant d s =
+  make_path (List.map id_of_string ("Coq" :: d)) (id_of_string s) CCI
 
 let bool_sp = coq_constant ["Init"; "Datatypes"] "bool"
 let coq_true = mkMutConstruct (((bool_sp,0),1), [||])
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index 5e0f9ad428..fc09cfa69c 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -561,7 +561,7 @@ open Vernac
 GEXTEND Gram
   Pcoq.Vernac_.vernac:
   [ [ IDENT "Global"; "Variable"; 
-      l = LIST1 IDENT SEP ","; ":"; t = type_v; "." ->
+      l = LIST1 ident SEP ","; ":"; t = type_v; "." ->
 	let idl = List.map Ast.nvar l in
 	let d = Ast.dynamic (in_typev t) in
 	  <:ast< (PROGVARIABLE (VERNACARGLIST ($LIST $idl)) (VERNACDYN $d)) >>