aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega/mutils.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega/mutils.ml')
-rw-r--r--plugins/micromega/mutils.ml12
1 files changed, 0 insertions, 12 deletions
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index c13e8fc28..b4c6d032b 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -294,18 +294,6 @@ struct
else XO (index (n lsr 1))
- let idx n =
- (*a.k.a path_of_int *)
- (* returns the list of digits of n in reverse order with initial 1 removed *)
- let rec digits_of_int n =
- if Int.equal n 1 then []
- else (Int.equal (n mod 2) 1)::(digits_of_int (n lsr 1))
- in
- List.fold_right
- (fun b c -> (if b then XI c else XO c))
- (List.rev (digits_of_int n))
- (XH)
-
let z x =
match compare x 0 with
| 0 -> Z0