From ffa57bae1e18fd52d63e8512a352ac63db15a7a9 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 6 Aug 2009 19:00:11 +0000
Subject: - Cleaning phase of the interfaces of libnames.ml and nametab.ml  
 (uniformisation of function names, classification). One of the most   visible
 change is the renaming of section_path into full_path (the   use of name
 section was obsolete due to the module system, but I   don't know if the new
 name is the best chosen one - especially it   remains some "sp" here and
 there). - Simplification of the interface of classify_object (first argument
 dropped). - Simplification of the code for vernac keyword "End". - Other
 small cleaning or dead code removal.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12265 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/cooking.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel')

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index a5cda5d133..edd3e498de 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -21,17 +21,17 @@ open Reduction
 
 type work_list = identifier array Cmap.t * identifier array KNmap.t
 
-let dirpath_prefix p = match repr_dirpath p with
+let pop_dirpath p = match repr_dirpath p with
   | [] -> anomaly "dirpath_prefix: empty dirpath"
   | _::l -> make_dirpath l
 
 let pop_kn kn =
   let (mp,dir,l) = Names.repr_kn kn in
-  Names.make_kn mp (dirpath_prefix dir) l
+  Names.make_kn mp (pop_dirpath dir) l
 
 let pop_con con = 
   let (mp,dir,l) = Names.repr_con con in
-  Names.make_con mp (dirpath_prefix dir) l
+  Names.make_con mp (pop_dirpath dir) l
 
 type my_global_reference =
   | ConstRef of constant
-- 
cgit v1.2.3