aboutsummaryrefslogtreecommitdiff
path: root/plugins/micromega/itv.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega/itv.ml')
-rw-r--r--plugins/micromega/itv.ml5
1 files changed, 3 insertions, 2 deletions
diff --git a/plugins/micromega/itv.ml b/plugins/micromega/itv.ml
index dc1df7ec9f..44cad820ed 100644
--- a/plugins/micromega/itv.ml
+++ b/plugins/micromega/itv.ml
@@ -11,10 +11,11 @@
(** Intervals (extracted from mfourier.ml) *)
open Num
+
(** The type of intervals is *)
type interval = num option * num option
- (** None models the absence of bound i.e. infinity *)
- (** As a result,
+ (** None models the absence of bound i.e. infinity
+ As a result,
- None , None -> \]-oo,+oo\[
- None , Some v -> \]-oo,v\]
- Some v, None -> \[v,+oo\[