diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-14 19:13:19 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-14 19:13:19 +0000 |
| commit | 8cc623262c625bda20e97c75f9ba083ae8e7760d (patch) | |
| tree | 3e7ef244636612606a574a21e4f8acaab828d517 /checker/term.ml | |
| parent | 6eaff635db797d1f9225b22196832c1bb76c0d94 (diff) | |
As r15801: putting everything from Util.array_* to CArray.*.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker/term.ml')
| -rw-r--r-- | checker/term.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/checker/term.ml b/checker/term.ml index a7fc0a8b8..b41bebca2 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -473,23 +473,23 @@ let compare_constr f t1 t2 = | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> f b1 b2 & f t1 t2 & f c1 c2 | App (c1,l1), App (c2,l2) -> if Array.length l1 = Array.length l2 then - f c1 c2 & array_for_all2 f l1 l2 + f c1 c2 & Array.for_all2 f l1 l2 else let (h1,l1) = decompose_app t1 in let (h2,l2) = decompose_app t2 in if List.length l1 = List.length l2 then f h1 h2 & List.for_all2 f l1 l2 else false - | Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & array_for_all2 f l1 l2 + | Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & Array.for_all2 f l1 l2 | Const c1, Const c2 -> eq_con_chk c1 c2 | Ind c1, Ind c2 -> eq_ind_chk c1 c2 | Construct (c1,i1), Construct (c2,i2) -> i1=i2 && eq_ind_chk c1 c2 | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> - f p1 p2 & f c1 c2 & array_for_all2 f bl1 bl2 + f p1 p2 & f c1 c2 & Array.for_all2 f bl1 bl2 | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) -> - ln1 = ln2 & array_for_all2 f tl1 tl2 & array_for_all2 f bl1 bl2 + ln1 = ln2 & Array.for_all2 f tl1 tl2 & Array.for_all2 f bl1 bl2 | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> - ln1 = ln2 & array_for_all2 f tl1 tl2 & array_for_all2 f bl1 bl2 + ln1 = ln2 & Array.for_all2 f tl1 tl2 & Array.for_all2 f bl1 bl2 | _ -> false let rec eq_constr m n = |