diff options
| author | ppedrot | 2012-11-08 17:11:59 +0000 |
|---|---|---|
| committer | ppedrot | 2012-11-08 17:11:59 +0000 |
| commit | b0b1710ba631f3a3a3faad6e955ef703c67cb967 (patch) | |
| tree | 9d35a8681cda8fa2dc968535371739684425d673 /kernel/closure.ml | |
| parent | bafb198e539998a4a64b2045a7e85125890f196e (diff) | |
Monomorphized a lot of equalities over OCaml integers, thanks to
the new Int module. Only the most obvious were removed, so there
are a lot more in the wild.
This may sound heavyweight, but it has two advantages:
1. Monomorphization is explicit, hence we do not miss particular
optimizations of equality when doing it carelessly with the generic
equality.
2. When we have removed all the generic equalities on integers, we
will be able to write something like "let (=) = ()" to retrieve all
its other uses (mostly faulty) spread throughout the code, statically.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15957 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/closure.ml')
| -rw-r--r-- | kernel/closure.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index 51e264106f..681fb8533d 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -354,7 +354,7 @@ and stack = stack_member list let empty_stack = [] let append_stack v s = - if Array.length v = 0 then s else + if Int.equal (Array.length v) 0 then s else match s with | Zapp l :: s -> Zapp (Array.append v l) :: s | _ -> Zapp v :: s @@ -398,7 +398,7 @@ let rec stack_assign s p c = match s with Zapp nargs :: s) | _ -> s let rec stack_tail p s = - if p = 0 then s else + if Int.equal p 0 then s else match s with | Zapp args :: s -> let q = Array.length args in @@ -719,7 +719,7 @@ let get_nth_arg head n stk = let bef = Array.sub args 0 n in let aft = Array.sub args (n+1) (q-n-1) in let stk' = - List.rev (if n = 0 then rstk else (Zapp bef :: rstk)) in + List.rev (if Int.equal n 0 then rstk else (Zapp bef :: rstk)) in (Some (stk', args.(n)), append_stack aft s') | Zupdate(m)::s -> strip_rec rstk (update m (h.norm,h.term)) n s @@ -764,7 +764,7 @@ let rec reloc_rargs_rec depth stk = | _ -> stk let reloc_rargs depth stk = - if depth = 0 then stk else reloc_rargs_rec depth stk + if Int.equal depth 0 then stk else reloc_rargs_rec depth stk let rec drop_parameters depth n argstk = match argstk with |