Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Semantic triggers #652

Closed
wants to merge 6 commits into from
Closed

Conversation

Halbaroth
Copy link
Collaborator

@Halbaroth Halbaroth added this to the 2.5.0 milestone Jun 14, 2023
@Halbaroth Halbaroth marked this pull request as draft June 14, 2023 15:10
bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this pull request Jun 19, 2023
This patch is an updated version of OCamlPro#652 to be compatible with the new
API in Dolmen for accessing the [in] semantic triggers.

In addition, the patch also adds proper support for theory extensions,
which were previously ignored by the dolmen frontend. There are also
some simple tests to ensure that theory extensions and semantic triggers
work.

It requires that Gbury/dolmen#162 and Gbury/dolmen#165 be merged to
work. It also includes OCamlPro#660 because it touches on similar codes and
there would be conflicts otherwise.
@bclement-ocp
Copy link
Collaborator

These changes are included in #662

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants