4 files changed, 5 insertions, 5 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index bbc4a0c5a..0677fa8df 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -248,7 +248,7 @@ type tactic_grammar = {
   tacgram_key : string;
   tacgram_level : int;
   tacgram_prods : grammar_prod_item list;
-  tacgram_tactic : dir_path * Tacexpr.glob_tactic_expr;
+  tacgram_tactic : Dir_path.t * Tacexpr.glob_tactic_expr;
 }
 
 type all_grammar_command =
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index 827e7c197..1cc890158 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -43,7 +43,7 @@ type tactic_grammar = {
   tacgram_key : string;
   tacgram_level : int;
   tacgram_prods : grammar_prod_item list;
-  tacgram_tactic : dir_path * Tacexpr.glob_tactic_expr;
+  tacgram_tactic : Dir_path.t * Tacexpr.glob_tactic_expr;
 }
 
 (** Adding notations *)
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 8e52a3bab..5f75a1d9e 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -18,7 +18,7 @@ let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"]
 let _ = List.iter Lexer.add_keyword prim_kw
 
 
-let local_make_qualid l id = make_qualid (make_dirpath l) id
+let local_make_qualid l id = make_qualid (Dir_path.make l) id
 
 let my_int_of_string loc s =
   try
@@ -101,7 +101,7 @@ GEXTEND Gram
   ;
   dirpath:
     [ [ id = ident; l = LIST0 field ->
-        make_dirpath (List.rev (id::l)) ] ]
+        Dir_path.make (List.rev (id::l)) ] ]
   ;
   string:
     [ [ s = STRING -> s ] ]
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index d1fd1edc7..a5f99a40b 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -174,7 +174,7 @@ module Prim :
     val reference : reference Gram.entry
     val by_notation : (Loc.t * string * string option) Gram.entry
     val smart_global : reference or_by_notation Gram.entry
-    val dirpath : dir_path Gram.entry
+    val dirpath : Dir_path.t Gram.entry
     val ne_string : string Gram.entry
     val ne_lstring : string located Gram.entry
     val var : Id.t located Gram.entry