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.

Sign up for GitHub

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

Jump to bottom

fix checking of uninstantiated metavariables in rules #301 #302

Merged
merged 7 commits into from Jan 10, 2020
Merged

fix checking of uninstantiated metavariables in rules #301 #302

merged 7 commits into from Jan 10, 2020

Conversation

fblanqui
Copy link
Member

No description provided.

@fblanqui
Copy link
Member Author

fblanqui commented Jan 7, 2020

Thanks @Rehan-MALAK or @rlepigre to review my PR! :-)

rlepigre
rlepigre reviewed Jan 8, 2020
View reviewed changes
Copy link
Contributor

@rlepigre rlepigre left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Mostly alright, I just gave a couple of comments! :)

src/extra.ml Outdated Show resolved Hide resolved
src/basics.ml Outdated Show resolved Hide resolved
src/terms.ml Outdated Show resolved Hide resolved
@Rehan-MALAK
Copy link
Contributor

Rehan-MALAK commented Jan 10, 2020 •
edited

I tried your branch rebased on my "model" branch Rehan-MALAK/lambdapi@7d3c621c (the one I use to actually formalize stuff in lambdapi) and I'm ok with it.
For the coding convention, it would be nice to have someday a git hook based on ocpindent or ocaml-format or something else because changing indentations messed up the git history.

Rehan-MALAK
Rehan-MALAK reviewed Jan 10, 2020
View reviewed changes
src/basics.ml Outdated Show resolved Hide resolved
@fblanqui
Copy link
Member Author

@Rehan-MALAK do you known how to install such a hook? If so, could you do this indeed?

@fblanqui fblanqui merged commit 54c1b30 into Deducteam:master Jan 10, 2020
@fblanqui fblanqui deleted the 301 branch January 10, 2020 17:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@rlepigre rlepigre rlepigre left review comments

@Rehan-MALAK Rehan-MALAK Rehan-MALAK left review comments

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@fblanqui @Rehan-MALAK @rlepigre