Skip to content

Commit

Permalink
Update docs/HowToFAQ/Errors-Parser.template
Browse files Browse the repository at this point in the history
Co-authored-by: Fabio Madge <[email protected]>
  • Loading branch information
RustanLeino and fabiomadge authored Jul 3, 2023
1 parent 086b484 commit e17b252
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion docs/HowToFAQ/Errors-Parser.template
Original file line number Diff line number Diff line change
Expand Up @@ -204,7 +204,7 @@ module N refines M { datatype D = ... Y | Z }

<!-- INSERT-TEXT -->

## **Error: datatype using traits is a beta feature; use /generalTraits:1 to engage** {#p_general_traits_beta}
## **Error: datatype extending traits is a beta feature; use /generalTraits:1 to engage** {#p_general_traits_beta}

```dafny
trait Trait { }
Expand Down

0 comments on commit e17b252

Please sign in to comment.