diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-02-28 15:18:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-02-28 21:52:16 +0100 |
| commit | d0eb3e2cd98bbeb08db3aa32d233233569d50351 (patch) | |
| tree | a93f71a39e922799a1755fc33b13c27fe0684551 /pretyping/term_dnet.ml | |
| parent | dc438047cc7d20d4f2df6ab703689814a7552623 (diff) | |
Removing Pervasives.compare in Termdn.
Diffstat (limited to 'pretyping/term_dnet.ml')
| -rw-r--r-- | pretyping/term_dnet.ml | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml index dd1309290..d22e032df 100644 --- a/pretyping/term_dnet.ml +++ b/pretyping/term_dnet.ml @@ -93,13 +93,7 @@ struct let compare cmp t1 t2 = match t1, t2 with | DRel, DRel -> 0 | DSort, DSort -> 0 - | DRef gr1, DRef gr2 -> - begin match gr1, gr2 with - | ConstRef c1, ConstRef c2 -> Constant.CanOrd.compare c1 c2 - | IndRef i1, IndRef i2 -> ind_ord i1 i2 - | ConstructRef c1, ConstructRef c2 -> constructor_ord c1 c2 - | _ -> Pervasives.compare gr1 gr2 (** OK **) - end + | DRef gr1, DRef gr2 -> RefOrdered.compare gr1 gr2 | DCtx (tl1, tr1), DCtx (tl2, tr2) | DLambda (tl1, tr1), DCtx (tl2, tr2) | DApp (tl1, tr1), DCtx (tl2, tr2) -> |