From 6b59b0f2a993c56cf0adc1d052a98b0df334a0f7 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 8 Oct 2011 12:44:59 +0000 Subject: Rely on kernel to know if a name is already used so as to be consistent with it. Maybe could we keep only the kernel check, but message would certainly need to be reformulated then. For instance, the message was previously different for an attempt to redefine a name whether this name was in the same section or not. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14528 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/libnames.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'library/libnames.ml') diff --git a/library/libnames.ml b/library/libnames.ml index c82b3476e..b91d24bd6 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -195,6 +195,7 @@ type full_path = { basename : identifier } let make_path pa id = { dirpath = pa; basename = id } + let repr_path { dirpath = pa; basename = id } = (pa,id) (* parsing and printing of section paths *) -- cgit v1.2.3