Skip to content

fixes #566 #595

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
Merged
CohenCyril merged 1 commit into from
Mar 23, 2022
Merged

fixes #566 #595

CohenCyril merged 1 commit into from
Mar 23, 2022

Conversation

@affeldt-aist
Copy link
Member

@affeldt-aist affeldt-aist commented Mar 11, 2022

Motivation for this change

fixes #566

Things done/to do
  • added corresponding entries in CHANGELOG_UNRELEASED.md
    - [ ] added corresponding documentation in the headers
Automatic note to reviewers

Read this Checklist and put a milestone if possible.

@affeldt-aist affeldt-aist added this to the 0.4.1 milestone Mar 11, 2022
CohenCyril
CohenCyril reviewed Mar 18, 2022
View reviewed changes
@affeldt-aist affeldt-aist force-pushed the measure_20220311 branch 2 times, most recently from d93ab0a to 233c5f3 Compare March 18, 2022 10:45
@affeldt-aist
Copy link
Member Author

affeldt-aist commented Mar 22, 2022

Here is an excerpt of the only CI error:

  # CAMLC -c src/coq_elpi_HOAS.ml
  # File "src/coq_elpi_HOAS.ml", line 616, characters 53-64:
  # Error: This expression has type Sorts.t
  #        but an expression was expected of type Univ.Universe.t
  # make[1]: *** [Makefile.coq:736: src/coq_elpi_HOAS.cmo] Error 2
  # make: *** [Makefile:38: build] Error 2

@affeldt-aist affeldt-aist mentioned this pull request Mar 22, 2022
Merged
2 tasks
@CohenCyril CohenCyril merged commit b012cf4 into master Mar 23, 2022
@affeldt-aist affeldt-aist deleted the measure_20220311 branch March 23, 2022 05:09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@CohenCyril CohenCyril CohenCyril left review comments

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

0.5.0

Development

Successfully merging this pull request may close these issues.

naming of measurable lemmas

3 participants

@affeldt-aist @CohenCyril