diff options
author | Stephane Glondu <steph@glondu.net> | 2011-04-19 16:47:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2011-04-19 16:47:51 +0200 |
commit | aa33547c764a229e22d323ca213d46ea221b903e (patch) | |
tree | 3894cb190f34bc1d2deee4322a674db641562ee0 /kernel/names.ml | |
parent | 50dc9067e98ca001ad2e875011abab5da6fdb621 (diff) | |
parent | 9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 (diff) |
Remove non-DFSG contentsupstream/8.3.pl2+dfsg
Diffstat (limited to 'kernel/names.ml')
-rw-r--r-- | kernel/names.ml | 8 |
1 files changed, 6 insertions, 2 deletions
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) |