From f42dd8d8530e6227621ccd662741f1da23700304 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Fri, 14 Dec 2012 15:57:08 +0000
Subject: Modulification of dir_path

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16072 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/extraction/modutil.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/extraction/modutil.ml')

diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index ca72a38ed1..9746c39e49 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -34,7 +34,7 @@ let se_iter do_decl do_spec do_mp =
 	let mp_w =
 	  List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl'
 	in
-	let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l')) in
+	let r = ConstRef (make_con mp_w Dir_path.empty (label_of_id l')) in
 	mt_iter mt; do_decl (Dtype(r,l,t))
     | MTwith (mt,ML_With_module(idl,mp))->
         let mp_mt = msid_of_mt mt in
-- 
cgit v1.2.3