diff options
| author |  puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-29 14:26:42 +0000 |
|---|---|---|
| committer | puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-29 14:26:42 +0000 |
| commit | f046e30fc712d193cfd708fa5313cb6dbf00080e (patch) | |
| tree | 15a097aa03ba99afe1c1911b4e890210de922046 /plugins/firstorder/sequent.ml | |
| parent | 9752cb8aa72d4fa5921592f095032db756dcb229 (diff) | |
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
Diffstat (limited to 'plugins/firstorder/sequent.ml')
| -rw-r--r-- | plugins/firstorder/sequent.ml | 10 |
1 files changed, 7 insertions, 3 deletions
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)) -> |