aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorGaëtan Gilbert2018-11-17 21:07:44 +0100
committerGaëtan Gilbert2019-03-14 15:46:16 +0100
commitab8c27c589ea90ac86518cc7c1b513b740190cdc (patch)
treeaea236e67ca897ab208ae95e352b29c9d3b28a58 /kernel
parent456919dd31f2f4bda15c6b37e4f1217bc085fc41 (diff)
Put [@inline] on CClosure.Mark functions
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cClosure.ml14
1 files changed, 7 insertions, 7 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 922fce957e..412637c4b6 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -307,32 +307,32 @@ module Mark : sig
end = struct
type t = int
- let of_state = function
+ let[@inline] of_state = function
| Norm -> 0b00 | Cstr -> 0b01 | Whnf -> 0b10 | Red -> 0b11
- let of_relevance = function
+ let[@inline] of_relevance = function
| Unknown -> 0
| KnownR -> 0b01
| KnownI -> 0b10
- let mark state relevance = (of_state state) * 4 + (of_relevance relevance)
+ let[@inline] mark state relevance = (of_state state) * 4 + (of_relevance relevance)
- let relevance x = match x land 0b11 with
+ let[@inline] relevance x = match x land 0b11 with
| 0b00 -> Unknown
| 0b01 -> KnownR
| 0b10 -> KnownI
| _ -> assert false
- let red_state x = match x land 0b1100 with
+ let[@inline] red_state x = match x land 0b1100 with
| 0b0000 -> Norm
| 0b0100 -> Cstr
| 0b1000 -> Whnf
| 0b1100 -> Red
| _ -> assert false
- let neutr x = x lor 0b1000 (* Whnf|Norm -> Whnf | Red|Cstr -> Red *)
+ let[@inline] neutr x = x lor 0b1000 (* Whnf|Norm -> Whnf | Red|Cstr -> Red *)
- let set_norm x = x land 0b0011
+ let[@inline] set_norm x = x land 0b0011
end
let mark = Mark.mark