From 9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Tue, 19 Apr 2011 16:44:20 +0200
Subject: Imported Upstream version 8.3.pl2

---
 kernel/names.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'kernel/names.ml')

diff --git a/kernel/names.ml b/kernel/names.ml
index 9f1becf7..e5a9f0fc 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: names.ml 13486 2010-10-03 17:01:43Z herbelin $ *)
+(* $Id: names.ml 13804 2011-01-27 00:41:34Z letouzey $ *)
 
 open Pp
 open Util
@@ -223,7 +223,7 @@ type constructor = inductive * int
 
 let constant_of_kn kn = (kn,kn)
 let constant_of_kn_equiv kn1 kn2 = (kn1,kn2)
-let make_con mp dir l = ((mp,dir,l),(mp,dir,l))
+let make_con mp dir l = constant_of_kn (mp,dir,l)
 let make_con_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l))
 let canonical_con con = snd con
 let user_con con = fst con
@@ -235,6 +235,10 @@ let debug_pr_con con = str "("++ pr_kn (fst con) ++ str ","++ pr_kn (snd con)++
 let eq_constant (_,kn1) (_,kn2) = kn1=kn2
 let debug_string_of_con con =  string_of_kn (fst con)^"'"^string_of_kn (snd con)
 
+let con_with_label ((mp1,dp1,l1),(mp2,dp2,l2) as con) lbl =
+  if lbl = l1 && lbl = l2 then con
+  else ((mp1,dp1,lbl),(mp2,dp2,lbl))
+
 let con_modpath con = modpath (fst con)
 
 let mind_modpath mind = modpath (fst mind)
-- 
cgit v1.2.3