From 43050b0d802f74fe59347f61830467a9804fd0d3 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 24 Oct 2013 21:25:12 +0000
Subject: Rtree : cleanup of the comparing code

 * Using generic fold functions was unecessarily obscure
 * No more List.mem and hence indirect use of ocaml generic comparison
 * Rtree.equiv (former Rtree.compare_rtree) has now a less cryptic
   semantic...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16934 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/inductive.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index e564feb692..e3e636e4aa 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -419,7 +419,7 @@ type subterm_spec =
   | Dead_code
   | Not_subterm
 
-let eq_wf_paths = Rtree.eq_rtree Declareops.eq_recarg
+let eq_wf_paths = Rtree.equal Declareops.eq_recarg
 
 let spec_of_tree t = lazy
   (if eq_wf_paths (Lazy.force t) mk_norec
-- 
cgit v1.2.3