diff options
| author |  Frédéric Besson <frederic.besson@inria.fr> | 2016-09-08 14:19:02 +0200 |
|---|---|---|
| committer | Frédéric Besson <frederic.besson@inria.fr> | 2016-09-08 14:19:02 +0200 |
| commit | 9f56baf7bb78a520dc2e7f5f0f94091ebf86dcaf (patch) | |
| tree | 692212e73e902b4aacf36f23ae5b375016979158 /plugins/micromega/mutils.ml | |
| parent | 76a8288c37e68fd8559f903af60abf8c3f87c007 (diff) | |
Fix Bug #5073 : regression of micromega plugin
The computed proof term is now more explicit exact (__arith P1 ... Pn X1 ... Xm)
instead of apply (__arith P1 ... Pn) which unification could fail.
Diffstat (limited to 'plugins/micromega/mutils.ml')
| -rw-r--r-- | plugins/micromega/mutils.ml | 12 |
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 |