diff options
| author | ppedrot | 2012-11-08 12:56:21 +0000 |
|---|---|---|
| committer | ppedrot | 2012-11-08 12:56:21 +0000 |
| commit | 5d87bcbb365e3fbdc0070abb31ab256b0f815165 (patch) | |
| tree | acb49f0d41371b87a970aea3d01de9f0491c2799 /kernel | |
| parent | b47498df42e23b99887a8df616d236029b839337 (diff) | |
Removing another bunch of generic equalities
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15955 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/names.ml | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index cbd66e03d4..96055ca16c 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -317,9 +317,9 @@ let make_mind_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l)) let canonical_mind mind = snd mind let user_mind mind = fst mind let repr_mind mind = fst mind -let mind_label mind= label (fst mind) +let mind_label mind = label (fst mind) -let eq_mind (_,kn1) (_,kn2) = kn1=kn2 +let eq_mind (_, kn1) (_, kn2) = kn_ord kn1 kn2 = 0 let string_of_mind mind = string_of_kn (fst mind) let pr_mind mind = str (string_of_mind mind) @@ -327,12 +327,14 @@ let debug_string_of_mind mind = "(" ^ string_of_kn (fst mind) ^ "," ^ string_of_kn (snd mind) ^ ")" let debug_pr_mind con = str (debug_string_of_mind con) -let ith_mutual_inductive (kn,_) i = (kn,i) -let ith_constructor_of_inductive ind i = (ind,i) -let inductive_of_constructor (ind,i) = ind -let index_of_constructor (ind,i) = i -let eq_ind (kn1,i1) (kn2,i2) = i1=i2&&eq_mind kn1 kn2 -let eq_constructor (kn1,i1) (kn2,i2) = i1=i2&&eq_ind kn1 kn2 +let ith_mutual_inductive (kn, _) i = (kn, i) +let ith_constructor_of_inductive ind i = (ind, i) +let inductive_of_constructor (ind, i) = ind +let index_of_constructor (ind, i) = i +let eq_ind (kn1, i1) (kn2, i2) = + i1 - i2 = 0 && eq_mind kn1 kn2 +let eq_constructor (kn1, i1) (kn2, i2) = + i1 - i2 = 0 && eq_ind kn1 kn2 module Mindmap = Map.Make(Canonical_ord) module Mindset = Set.Make(Canonical_ord) |