From f046e30fc712d193cfd708fa5313cb6dbf00080e Mon Sep 17 00:00:00 2001 From: puech Date: Fri, 29 Jul 2011 14:26:42 +0000 Subject: Sequent: generic equality on kernel_name replaced by kn_ord git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14338 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/firstorder/sequent.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'plugins/firstorder/sequent.ml') diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 85324e71a..b93a58b34 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -102,9 +102,13 @@ let compare_constr_int f t1 t2 = (f =? (compare_list f)) c1 c2 l1 l2 | Evar (e1,l1), Evar (e2,l2) -> ((-) =? (compare_array f)) e1 e2 l1 l2 - | Const c1, Const c2 -> Pervasives.compare c1 c2 - | Ind c1, Ind c2 -> Pervasives.compare c1 c2 - | Construct c1, Construct c2 -> Pervasives.compare c1 c2 + | Const c1, Const c2 -> kn_ord (canonical_con c1) (canonical_con c2) + | Ind (spx, ix), Ind (spy, iy) -> + let c = ix - iy in if c = 0 then kn_ord (canonical_mind spx) (canonical_mind spy) else c + | Construct ((spx, ix), jx), Construct ((spy, iy), jy) -> + let c = jx - jy in if c = 0 then + (let c = ix - iy in if c = 0 then kn_ord (canonical_mind spx) (canonical_mind spy) else c) + else c | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> ((f =? f) ==? (compare_array f)) p1 p2 c1 c2 bl1 bl2 | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) -> -- cgit v1.2.3