summaryrefslogtreecommitdiff
path: root/plugins/micromega
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
commit2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch)
tree074182834cb406d1304aec4233718564a9c06ba1 /plugins/micromega
parent0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff)
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'plugins/micromega')
-rw-r--r--plugins/micromega/mfourier.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml
index 88c1a783..a36369d2 100644
--- a/plugins/micromega/mfourier.ml
+++ b/plugins/micromega/mfourier.ml
@@ -23,7 +23,7 @@ struct
- None , Some v -> \]-oo,v\]
- Some v, None -> \[v,+oo\[
- Some v, Some v' -> \[v,v'\]
- Intervals needs to be explicitely normalised.
+ Intervals needs to be explicitly normalised.
*)
type who = Left | Right