From f5066f761de29d3e77194cf065187413bd473e15 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 15 Apr 2024 13:23:50 -0700 Subject: [PATCH] FStar.Real: remove mistakenly-added to_string Thanks @gebner --- ulib/FStar.Real.fsti | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/ulib/FStar.Real.fsti b/ulib/FStar.Real.fsti index 807bfca53cb..f4f265aeb6a 100644 --- a/ulib/FStar.Real.fsti +++ b/ulib/FStar.Real.fsti @@ -25,7 +25,7 @@ module FStar.Real This is only a logical model of the reals. There is no extraction for them, as they are an erasable type. Any operation that can observe - a real (comparisons, to_string, etc) must be Ghost or a proposition. + a real (comparisons, etc) must be Ghost or a proposition. *) [@@erasable] @@ -33,8 +33,6 @@ val real : Type0 val of_int : int -> Tot real -val to_string: real -> GTot string - val ( +. ) : real -> real -> Tot real val ( -. ) : real -> real -> Tot real val ( *. ) : real -> real -> Tot real