diff --git a/CHANGES.md b/CHANGES.md
index 5ca0770e3..9f65828f2 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -70,6 +70,9 @@ next
   match on builtins, especially wrt to completeness of pattern matching.
   Also is likely to have a small performance improvement. (PR#240)
 
+- Separate floating-point rounding modes into their own
+  `Builtin.Float.rounding_mode` type, so that pattern matching over
+  rounding modes can be exhaustive on its own (PR#271)
 
 v0.10
 -----
diff --git a/src/languages/smtlib2/print/print.ml b/src/languages/smtlib2/print/print.ml
index 01d07c8b4..dfc96de9a 100644
--- a/src/languages/smtlib2/print/print.ml
+++ b/src/languages/smtlib2/print/print.ml
@@ -842,11 +842,11 @@ module Make(Config : Config)(Lexer : Lexer with type token := Config.token) = st
         begin match blt with
           | T _ | RoundingMode -> assert false (* cannot occur in terms *)
           | Fp _ -> simple "fp"
-          | RoundNearestTiesToEven -> simple "RNE"
-          | RoundNearestTiesToAway -> simple "RNA"
-          | RoundTowardPositive -> simple "RTP"
-          | RoundTowardNegative -> simple "RTN"
-          | RoundTowardZero -> simple "RTZ"
+          | RM RoundNearestTiesToEven -> simple "RNE"
+          | RM RoundNearestTiesToAway -> simple "RNA"
+          | RM RoundTowardPositive -> simple "RTP"
+          | RM RoundTowardNegative -> simple "RTN"
+          | RM RoundTowardZero -> simple "RTZ"
           | Abs _ -> simple "fp.abs"
           | Neg _ -> simple "fp.neg"
           | Add _ -> simple "fp.add"
diff --git a/src/model/fp.ml b/src/model/fp.ml
index e8bd00be1..130a8dc34 100644
--- a/src/model/fp.ml
+++ b/src/model/fp.ml
@@ -123,11 +123,11 @@ let builtins ~eval env (cst : Dolmen.Std.Expr.Term.Const.t) =
   | Dolmen.Std.Builtin.Float blt ->
     begin match blt with
       | T _ | RoundingMode -> assert false (* Types are not evaluated *)
-      | RoundNearestTiesToEven -> Some (Value.mk ~ops:ops_rm Mode.NE)
-      | RoundNearestTiesToAway -> Some (Value.mk ~ops:ops_rm Mode.NA)
-      | RoundTowardPositive -> Some (Value.mk ~ops:ops_rm Mode.UP)
-      | RoundTowardNegative -> Some (Value.mk ~ops:ops_rm Mode.DN)
-      | RoundTowardZero -> Some (Value.mk ~ops:ops_rm Mode.ZR)
+      | RM RoundNearestTiesToEven -> Some (Value.mk ~ops:ops_rm Mode.NE)
+      | RM RoundNearestTiesToAway -> Some (Value.mk ~ops:ops_rm Mode.NA)
+      | RM RoundTowardPositive -> Some (Value.mk ~ops:ops_rm Mode.UP)
+      | RM RoundTowardNegative -> Some (Value.mk ~ops:ops_rm Mode.DN)
+      | RM RoundTowardZero -> Some (Value.mk ~ops:ops_rm Mode.ZR)
       | Of_real { e = ew; s = prec; } ->
         Some (Fun.mk_clos @@ Fun.fun_2 ~cst (fun m r ->
             check ~ew ~mw:(prec - 1);
diff --git a/src/standard/builtin.ml b/src/standard/builtin.ml
index 673df0284..0be469c86 100644
--- a/src/standard/builtin.ml
+++ b/src/standard/builtin.ml
@@ -175,15 +175,19 @@ type 'a t += Bitv of 'a Bitv.t
 (* ************************************************************************* *)
 
 module Float = struct
-  type _ t =
-    | T of { e : int; s : int; }
-    | RoundingMode
-    | Fp of { e : int; s : int; }
+
+  type rounding_mode =
     | RoundNearestTiesToEven
     | RoundNearestTiesToAway
     | RoundTowardPositive
     | RoundTowardNegative
     | RoundTowardZero
+
+  type _ t =
+    | T of { e : int; s : int; }
+    | RoundingMode
+    | RM of rounding_mode
+    | Fp of { e : int; s : int; }
     | Plus_infinity of { e : int; s : int; }
     | Minus_infinity of { e : int; s : int; }
     | Plus_zero of { e : int; s : int; }
diff --git a/src/standard/builtin.mli b/src/standard/builtin.mli
index 92f92c75f..0ef52238b 100644
--- a/src/standard/builtin.mli
+++ b/src/standard/builtin.mli
@@ -543,6 +543,19 @@ type 'a t += Bitv of 'a Bitv.t
 (*  ************************************************************************* *)
 
 module Float : sig
+
+  type rounding_mode =
+    | RoundNearestTiesToEven
+    (** [RoundNearestTiesToEven : RoundingMode]: *)
+    | RoundNearestTiesToAway
+    (** [RoundNearestTiesToAway : RoundingMode]: *)
+    | RoundTowardPositive
+    (** [RoundTowardPositive : RoundingMode *)
+    | RoundTowardNegative
+    (** [RoundTowardNegative : RoundingMode *)
+    | RoundTowardZero
+    (** [RoundTowardZero : RoundingMode *)
+
   type _ t =
     | T of { e : int; s : int; }
     (** [Float(e,s): ttype]: type constructor for floating point of exponent of
@@ -550,20 +563,12 @@ module Float : sig
         greater than 1 *)
     | RoundingMode
     (** [RoundingMode: ttype]: type for enumerated type of rounding modes. *)
+    | RM of rounding_mode
+    (** [RM r: RoundingMode]: rounding mode literals. *)
     | Fp of { e : int; s : int; }
     (** [Fp(e, s): Bitv.T{1} -> Bitv.T{e} -> Bitv.T{s-1} -> Fp(e,s)]: bitvector literal.
         The IEEE-format is used for the conversion [sb^se^ss].
         All the NaN are converted to the same value. *)
-    | RoundNearestTiesToEven
-    (** [RoundNearestTiesToEven : RoundingMode]: *)
-    | RoundNearestTiesToAway
-    (** [RoundNearestTiesToAway : RoundingMode]: *)
-    | RoundTowardPositive
-    (** [RoundTowardPositive : RoundingMode *)
-    | RoundTowardNegative
-    (** [RoundTowardNegative : RoundingMode *)
-    | RoundTowardZero
-    (** [RoundTowardZero : RoundingMode *)
     | Plus_infinity of { e: int; s : int; }
     (** [Plus_infinity{e;s} : Fp{e;s}] *)
     | Minus_infinity of { e : int; s : int; }
diff --git a/src/standard/expr.ml b/src/standard/expr.ml
index ebb5fdab9..ab493c6a4 100644
--- a/src/standard/expr.ml
+++ b/src/standard/expr.ml
@@ -2620,19 +2620,19 @@ module Term = struct
           )
 
       let roundNearestTiesToEven =
-        mk' ~builtin:(Builtin.Float RoundNearestTiesToEven) "RoundNearestTiesToEven" [] [] Ty.roundingMode
+        mk' ~builtin:(Builtin.Float (RM RoundNearestTiesToEven)) "RoundNearestTiesToEven" [] [] Ty.roundingMode
 
       let roundNearestTiesToAway =
-        mk' ~builtin:(Builtin.Float RoundNearestTiesToAway) "RoundNearestTiesToAway" [] [] Ty.roundingMode
+        mk' ~builtin:(Builtin.Float (RM RoundNearestTiesToAway)) "RoundNearestTiesToAway" [] [] Ty.roundingMode
 
       let roundTowardPositive =
-        mk' ~builtin:(Builtin.Float RoundTowardPositive) "RoundTowardPositive" [] [] Ty.roundingMode
+        mk' ~builtin:(Builtin.Float (RM RoundTowardPositive)) "RoundTowardPositive" [] [] Ty.roundingMode
 
       let roundTowardNegative =
-        mk' ~builtin:(Builtin.Float RoundTowardNegative) "RoundTowardNegative" [] [] Ty.roundingMode
+        mk' ~builtin:(Builtin.Float (RM RoundTowardNegative)) "RoundTowardNegative" [] [] Ty.roundingMode
 
       let roundTowardZero =
-        mk' ~builtin:(Builtin.Float RoundTowardZero) "RoundTowardZero" [] [] Ty.roundingMode
+        mk' ~builtin:(Builtin.Float (RM RoundTowardZero)) "RoundTowardZero" [] [] Ty.roundingMode
 
       (** Generic function for creating functions primarily on the same floating
           point format with optionally a rounding mode and a particular result