Skip to content

Commit

Permalink
Fix parser
Browse files Browse the repository at this point in the history
In preparation for FStarLang/FStar#3317
  • Loading branch information
mtzguido committed Jun 17, 2024
1 parent 9285417 commit 96441f0
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions src/ocaml/plugin/FStar_Parser_Parse.mly
Original file line number Diff line number Diff line change
Expand Up @@ -1150,7 +1150,7 @@ tmArrow(Tm):
| dom=tmArrowDomain(Tm) RARROW tgt=tmArrow(Tm)
{
let ((aq_opt, attrs), dom_tm) = dom in
let b = match extract_named_refinement dom_tm with
let b = match extract_named_refinement true dom_tm with
| None -> mk_binder_with_attrs (NoName dom_tm) (rr $loc(dom)) Un aq_opt attrs
| Some (x, t, f) -> mkRefinedBinder x t true f (rr2 $loc(dom) $loc(dom)) aq_opt attrs
in
Expand All @@ -1162,7 +1162,7 @@ simpleArrow:
| dom=simpleArrowDomain RARROW tgt=simpleArrow
{
let ((aq_opt, attrs), dom_tm) = dom in
let b = match extract_named_refinement dom_tm with
let b = match extract_named_refinement true dom_tm with
| None -> mk_binder_with_attrs (NoName dom_tm) (rr $loc(dom)) Un aq_opt attrs
| Some (x, t, f) -> mkRefinedBinder x t true f (rr2 $loc(dom) $loc(dom)) aq_opt attrs
in
Expand Down Expand Up @@ -1240,7 +1240,7 @@ tmNoEqWith(X):
| e1=tmNoEqWith(X) AMP e2=tmNoEqWith(X)
{
let dom =
match extract_named_refinement e1 with
match extract_named_refinement false e1 with
| Some (x, t, f) ->
let dom = mkRefinedBinder x t true f (rr $loc(e1)) None [] in
Inl dom
Expand Down

0 comments on commit 96441f0

Please sign in to comment.