From 067aa9a444b7d13733c8ca1cf52d6d73e105dec0 Mon Sep 17 00:00:00 2001
From: barras
Date: Tue, 18 Mar 2008 13:30:57 +0000
Subject: improved the implementation of rtree

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

(limited to 'kernel/inductive.ml')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index aef3d6cc82..f60e2dbe0f 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -425,8 +425,8 @@ type subterm_spec =
   | Not_subterm
 
 let spec_of_tree t =
-  if t=mk_norec then Not_subterm else Subterm(Strict,t)
-
+  if Rtree.eq_rtree (=) t mk_norec then Not_subterm else Subterm(Strict,t)
+ 
 let subterm_spec_glb =
   let glb2 s1 s2 =
     match s1,s2 with
@@ -435,7 +435,7 @@ let subterm_spec_glb =
       | Not_subterm, _ -> Not_subterm
       | _, Not_subterm -> Not_subterm
       | Subterm (a1,t1), Subterm (a2,t2) ->
-          if t1=t2 then Subterm (size_glb a1 a2, t1)
+          if Rtree.eq_rtree (=) t1 t2 then Subterm (size_glb a1 a2, t1)
           (* branches do not return objects with same spec *)
           else Not_subterm in
   Array.fold_left glb2 Dead_code
-- 
cgit v1.2.3