Commit 5ba7dc20 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Add backward-compatible notations for rounding modes.

Type of rounding mode is changed from 1.4, but expressions like
"round beta rndMODE" are still usable.
parent 4d6b7ebc
......@@ -1854,3 +1854,9 @@ End Inclusion.
End Generic.
Notation ZnearestA := (Znearest (Zle_bool 0)).
(** Notations for backward-compatibility with Flocq 1.4. *)
Notation rndDN := Zfloor (only parsing).
Notation rndUP := Zceil (only parsing).
Notation rndZR := Ztrunc (only parsing).
Notation rndNA := ZnearestA (only parsing).
......@@ -526,3 +526,6 @@ now apply round_NE_pt_pos.
Qed.
End Fcore_rnd_NE.
(** Notations for backward-compatibility with Flocq 1.4. *)
Notation rndNE := ZnearestE (only parsing).
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment