Skip to content

Commit

Permalink
Merge pull request #948 from hacspec/eliminate-error-message-issue-463
Browse files Browse the repository at this point in the history
fix(engine/f*): convert an unimplemented to an assertion failure
  • Loading branch information
maximebuyse authored Oct 2, 2024
2 parents 9321a24 + 33c2e4d commit d6535c5
Showing 1 changed file with 3 additions and 2 deletions.
5 changes: 3 additions & 2 deletions engine/backends/fstar/fstar_backend.ml
Original file line number Diff line number Diff line change
Expand Up @@ -405,8 +405,9 @@ struct
| POr { subpats } when shallow ->
F.pat @@ F.AST.PatOr (List.map ~f:ppat subpats)
| POr _ ->
Error.unimplemented ~issue_id:463 p.span
~details:"The F* backend doesn't support nested disjuntive patterns"
Error.assertion_failure p.span
"Nested disjuntive patterns should have been eliminated by phase \
`HoistDisjunctions` (see PR #830)."
| PArray { args } -> F.pat @@ F.AST.PatList (List.map ~f:ppat args)
| PConstruct { name = `TupleCons 0; args = [] } ->
F.pat @@ F.AST.PatConst F.Const.Const_unit
Expand Down

0 comments on commit d6535c5

Please sign in to comment.