aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
authorppedrot2012-12-13 14:49:35 +0000
committerppedrot2012-12-13 14:49:35 +0000
commit989d7d5f4d3d023704935f2db49090b9ac4b2e13 (patch)
treec1f73dd93200d63e3373cf6db354d4aacd11dc68 /tactics
parentde08c197502d6e7c7c43c3b16f3bea9c9e504662 (diff)
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
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index a462460a5d..49841ecfab 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -117,7 +117,7 @@ type search_entry = stored_data list * stored_data list * Bounded_net.t
let empty_se = ([],[],Bounded_net.create ())
let eq_pri_auto_tactic (_, x) (_, y) =
- if Int.equal x.pri y.pri && Option.Misc.compare constr_pattern_eq x.pat y.pat then
+ if Int.equal x.pri y.pri && Option.equal constr_pattern_eq x.pat y.pat then
match x.code,y.code with
| Res_pf(cstr,_),Res_pf(cstr1,_) ->
eq_constr cstr cstr1