From 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Thu, 19 Jan 2006 22:34:29 +0000 Subject: Imported Upstream version 8.0pl3 --- library/nametab.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'library/nametab.mli') diff --git a/library/nametab.mli b/library/nametab.mli index 08a9d1bb..4cea1d40 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: nametab.mli,v 1.43.2.2 2005/01/21 16:41:51 herbelin Exp $ i*) +(*i $Id: nametab.mli,v 1.43.2.3 2005/11/21 09:16:27 herbelin Exp $ i*) (*i*) open Util @@ -144,7 +144,7 @@ val full_name_module : qualid -> dir_path val sp_of_syntactic_definition : kernel_name -> section_path val shortest_qualid_of_global : Idset.t -> global_reference -> qualid -val shortest_qualid_of_syndef : kernel_name -> qualid +val shortest_qualid_of_syndef : Idset.t -> kernel_name -> qualid val shortest_qualid_of_tactic : ltac_constant -> qualid val dir_of_mp : module_path -> dir_path -- cgit v1.2.3