diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-27 19:20:27 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-09-27 19:20:27 +0000 |
| commit | 11ca3113365639136cf65a74c345080a9434e69b (patch) | |
| tree | da263c149cd1e90bde14768088730e48e78e4776 /kernel/constr.ml | |
| parent | ee2f85396fa0cef65bc4295b5ac6c259e83df134 (diff) | |
Removing a bunch of generic equalities.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/constr.ml')
| -rw-r--r-- | kernel/constr.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index f751343bc..f2d66f03a 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -365,6 +365,9 @@ let rec eq_constr m n = let equal m n = eq_constr m n (* to avoid tracing a recursive fun *) +(** We only use this function over blocks! *) +let tag t = Obj.tag (Obj.repr t) + let constr_ord_int f t1 t2 = let (=?) f g i1 i2 j1 j2= let c = f i1 i2 in @@ -403,7 +406,7 @@ let constr_ord_int f t1 t2 = | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> ((Int.compare =? (Array.compare f)) ==? (Array.compare f)) ln1 ln2 tl1 tl2 bl1 bl2 - | t1, t2 -> Pervasives.compare t1 t2 + | t1, t2 -> Int.compare (tag t1) (tag t2) let rec compare m n= constr_ord_int compare m n |