Skip to content

[declare] Hide internals of variable declaration entries. - #12440

Merged
SkySkimmer merged 1 commit into
rocq-prover:masterfrom
ejgallego:proof+local_private
Jun 4, 2020
Merged

[declare] Hide internals of variable declaration entries.#12440
SkySkimmer merged 1 commit into
rocq-prover:masterfrom
ejgallego:proof+local_private

Conversation

@ejgallego

@ejgallego ejgallego commented Jun 3, 2020

Copy link
Copy Markdown
Contributor

In particular this avoids exposing Evd.side_effects proof_entry in
the API.

@ejgallego ejgallego added kind: cleanup Code removal, deprecation, refactorings, etc. kind: internal API, ML documentation... labels Jun 3, 2020
@ejgallego ejgallego added this to the 8.13+beta1 milestone Jun 3, 2020
@ejgallego
ejgallego requested a review from a team as a code owner June 3, 2020 14:43
SkySkimmer
SkySkimmer reviewed Jun 3, 2020
View reviewed changes
Comment thread vernac/declare.mli Outdated
SkySkimmer
SkySkimmer reviewed Jun 3, 2020
View reviewed changes
Comment thread vernac/declare.ml Outdated
@SkySkimmer
SkySkimmer requested a review from a team June 3, 2020 14:51
@ejgallego
[declare] Hide internals of variable declaration entries.
6fe12fd 
In particular this avoids exposing `Evd.side_effects proof_entry` in
the API.
@ejgallego
ejgallego force-pushed the proof+local_private branch from 6598950 to 6fe12fd Compare June 3, 2020 15:37
SkySkimmer
SkySkimmer reviewed Jun 3, 2020
View reviewed changes
Comment thread vernac/declare.mli
@SkySkimmer SkySkimmer self-assigned this Jun 3, 2020
@SkySkimmer SkySkimmer added needs: overlay This is breaking external developments we track in CI. and removed needs: overlay This is breaking external developments we track in CI. labels Jun 3, 2020
@ejgallego

ejgallego commented Jun 3, 2020

Copy link
Copy Markdown
Contributor Author

Quickchick seems still broken:

 + cd /builds/coq/coq/_build_ci/ext_lib
 + make
 + '[' -z x ']'
 + command make
 + make
 make[1]: Entering directory '/builds/coq/coq/_build_ci/ext_lib'
 make -f 
 make: option requires an argument -- 'f'

@SkySkimmer

SkySkimmer commented Jun 3, 2020

Copy link
Copy Markdown
Contributor

Even after rocq-community/coq-ext-lib#92 ?

@ejgallego

ejgallego commented Jun 4, 2020

Copy link
Copy Markdown
Contributor Author

Even after coq-community/coq-ext-lib#92 ?

Seems so, let me re-run again.

@ejgallego

ejgallego commented Jun 4, 2020

Copy link
Copy Markdown
Contributor Author

Seems so, let me re-run again.

I dunno what happened, it works now.

@SkySkimmer

SkySkimmer commented Jun 4, 2020

Copy link
Copy Markdown
Contributor

Probably just a race.

@SkySkimmer
SkySkimmer merged commit 0ae2017 into rocq-prover:master Jun 4, 2020
@ejgallego
ejgallego deleted the proof+local_private branch June 4, 2020 11:37
@ejgallego

ejgallego commented Jun 4, 2020

Copy link
Copy Markdown
Contributor Author

Thanks!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@SkySkimmer SkySkimmer SkySkimmer approved these changes

Assignees

@SkySkimmer SkySkimmer

Labels

kind: cleanup Code removal, deprecation, refactorings, etc. kind: internal API, ML documentation...

Projects

None yet

Milestone

8.13+beta1

Development

Successfully merging this pull request may close these issues.

2 participants

@ejgallego @SkySkimmer