From a452fbed5123ccfd0a341bd1f7bcc3bc18b44a9b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 17 Sep 2024 10:19:33 -0700 Subject: [PATCH] range now has def_range --- .../bug-reports/error-messages/Bug.DesugaringError.fst.expected | 1 + 1 file changed, 1 insertion(+) diff --git a/share/pulse/examples/bug-reports/error-messages/Bug.DesugaringError.fst.expected b/share/pulse/examples/bug-reports/error-messages/Bug.DesugaringError.fst.expected index df00f4946..b97a2ce1a 100644 --- a/share/pulse/examples/bug-reports/error-messages/Bug.DesugaringError.fst.expected +++ b/share/pulse/examples/bug-reports/error-messages/Bug.DesugaringError.fst.expected @@ -23,6 +23,7 @@ * Error 189 at Bug.DesugaringError.fst(31,9-31,10): - Expected expression of type Prims.nat got expression y of type Prims.bool - Raised within Tactics.refl_instantiate_implicits + - See also Bug.DesugaringError.fst(31,4-31,10) >>] >> Got issues: [