From 858e76c13dc9421f1c681511bfc1b7f2cc7a0884 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Fri, 15 Aug 2025 11:33:26 -0700
Subject: [PATCH 1/2] Update F* parser

Just a simple range fix
---
 src/ml/FStarC_Parser_Parse.mly | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/ml/FStarC_Parser_Parse.mly b/src/ml/FStarC_Parser_Parse.mly
index 8dd071271..a439fbc2e 100644
--- a/src/ml/FStarC_Parser_Parse.mly
+++ b/src/ml/FStarC_Parser_Parse.mly
@@ -419,8 +419,8 @@ rawDecl:
       {
         let r = rr $loc in
         let lbs = focusLetBindings lbs r in
-        if q <> Rec && List.length lbs <> 1
-        then raise_error_text r Fatal_MultipleLetBinding "Unexpected multiple let-binding (Did you forget some rec qualifier ?)";
+        if q <> Rec && FStarC_List.length lbs > Prims.parse_int "1"
+        then raise_error_text (fst (nth lbs (Prims.parse_int "1"))).prange Fatal_MultipleLetBinding "Unexpected multiple let-binding (Did you forget some rec qualifier ?)";
         TopLevelLet(q, lbs)
       }
   | VAL c=constant

From ca67af74e2195776ade34c1eb6f1cace13a7b46c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Fri, 15 Aug 2025 11:30:01 -0700
Subject: [PATCH 2/2] parser: allow nested quantifiers at the top level

Note: the parser is spitting out a lot of conflicts.

	Warning: 28 states have shift/reduce conflicts.
	Warning: one state has reduce/reduce conflicts.
	Warning: 338 shift/reduce conflicts were arbitrarily resolved.
	Warning: one reduce/reduce conflict was arbitrarily resolved.
	Warning: 232 end-of-stream conflicts were arbitrarily resolved.

These are not introduced (nor fixed) by this patch.
---
 src/ml/pulseparser.mly       |  8 ++++----
 test/nolib/QuantifierOps.fst | 26 ++++++++++++++++++++++++++
 2 files changed, 30 insertions(+), 4 deletions(-)
 create mode 100644 test/nolib/QuantifierOps.fst

diff --git a/src/ml/pulseparser.mly b/src/ml/pulseparser.mly
index 12afa1205..592490c43 100644
--- a/src/ml/pulseparser.mly
+++ b/src/ml/pulseparser.mly
@@ -359,10 +359,10 @@ mutOrRefQualifier:
   | MUT { MUT }
   | REF { REF }
 
-typX(X,Y):
-  | t=Y { t }
+typX(X):
+  | t=X { t }
 
-  | q=quantifier bs=binders DOT trigger=trigger e=X
+  | q=quantifier bs=binders DOT trigger=trigger e=typX(X)
       {
         match bs with
         | [] ->
@@ -373,5 +373,5 @@ typX(X,Y):
       }
 
 pulseSLProp:
-  | p=typX(tmEqWith(appTermNoRecordExp), tmEqWith(appTermNoRecordExp))
+  | p=typX(tmEqWith(appTermNoRecordExp))
     { p }
diff --git a/test/nolib/QuantifierOps.fst b/test/nolib/QuantifierOps.fst
new file mode 100644
index 000000000..f7d8ed556
--- /dev/null
+++ b/test/nolib/QuantifierOps.fst
@@ -0,0 +1,26 @@
+module QuantifierOps
+
+#lang-pulse
+open Pulse.Nolib
+
+let ( exists* ) : #a:Type -> (a -> slprop) -> slprop = admit()
+let ( forall+ ) : #a:Type -> (a -> slprop) -> slprop = admit()
+
+let test =
+  forall+ (x : int).
+    exists* (y : int).
+      emp
+
+let test2 =
+  exists* (y : int).
+    forall+ (x : int).
+      emp
+
+fn def ()
+  preserves
+    forall+ (x : int).
+      exists* (y : int).
+        emp
+{
+  ()
+}