From b731edadffd527a907a6aa4b5a420b6a8dbe4690 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 12 Nov 2001 12:55:38 +0000
Subject: petit oups

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2184 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/common.mli     | 2 ++
 contrib/extraction/extract_env.ml | 2 +-
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli
index 122075c87f..c9b41a4efe 100644
--- a/contrib/extraction/common.mli
+++ b/contrib/extraction/common.mli
@@ -15,6 +15,8 @@ open Nametab
 
 module ToplevelPp : Mlpp
 
+val sp_of_r : global_reference -> section_path
+
 val module_of_r : global_reference -> identifier
 
 val extract_to_file : 
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index a0ca727e0c..6969c412a8 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -157,7 +157,7 @@ let print_user_extract r =
 let decl_in_r r0 = function 
   | Dglob (r,_) -> r = r0
   | Dabbrev (r,_,_) -> r = r0
-  | Dtype ((_,r,_)::_, _) -> r = r0
+  | Dtype ((_,r,_)::_, _) -> sp_of_r r = sp_of_r r0
   | Dtype ([],_) -> false
   | Dcustom (r,_) ->  r = r0 
 
-- 
cgit v1.2.3