From 989d7d5f4d3d023704935f2db49090b9ac4b2e13 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Thu, 13 Dec 2012 14:49:35 +0000
Subject: Renamed Option.Misc.compare to the more uniform Option.equal.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16063 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/patternops.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 0c21cb805c..8e4351deb0 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -23,8 +23,8 @@ open Evd
 
 let case_info_pattern_eq i1 i2 =
   i1.cip_style == i2.cip_style &&
-  Option.Misc.compare eq_ind i1.cip_ind i2.cip_ind &&
-  Option.Misc.compare Int.equal i1.cip_ind_args i2.cip_ind_args &&
+  Option.equal eq_ind i1.cip_ind i2.cip_ind &&
+  Option.equal Int.equal i1.cip_ind_args i2.cip_ind_args &&
   i1.cip_extensible == i2.cip_extensible
 
 let rec constr_pattern_eq p1 p2 = match p1, p2 with
@@ -45,7 +45,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
 | PLetIn (v1, t1, b1), PLetIn (v2, t2, b2) ->
   name_eq v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2
 | PSort s1, PSort s2 -> glob_sort_eq s1 s2
-| PMeta m1, PMeta m2 -> Option.Misc.compare id_eq m1 m2
+| PMeta m1, PMeta m2 -> Option.equal id_eq m1 m2
 | PIf (t1, l1, r1), PIf (t2, l2, r2) ->
   constr_pattern_eq t1 t2 && constr_pattern_eq l1 l2 && constr_pattern_eq r1 r2
 | PCase (info1, p1, r1, l1), PCase (info2, p2, r2, l2) ->
-- 
cgit v1.2.3