[declare] Refactor constant information into a record. - #12372

Merged

SkySkimmer merged 28 commits into

rocq-prover:masterfrom

ejgallego:proof+info

Jun 29, 2020

Commits on Jun 26, 2020

[declare] Stronger typing for start_proof
ejgallego
committed
f77743c
[declare] Move proof information to declare.
ejgallego
committed
43d381a
[declare] Remove mutual internals from Info.t structure.
ejgallego
committed
2ac5353
[declare] Remove Lemmas module
ejgallego
committed
671004a
[declare] Refactor constant information into a record.
ejgallego
committed
1f121eb
[declare] Make ProgramDecl.t abstract
ejgallego
committed
7d183d8
[declare] [api] Removal of deprecated functions
ejgallego
committed
d83e95c
[declare] [api] Removal of duplicated type aliases.
ejgallego
committed
a6d663c
[declare] Move udecl to Info structure.
ejgallego
committed
b143d12
[declare] Reify Proof.t API into the Proof module.
ejgallego
committed
030bb57
[declare] [api] Modify logical presentation of declare interfaces
ejgallego
committed
c09871d
[declare] [compat] Remove exception alias.
ejgallego
committed
6291e5b
[declare] Documentation on obligations
ejgallego
committed
9c58cd6
[declare] Nit on interface
ejgallego
committed
ba8db3c
[declare] Nit on hook call.
ejgallego
committed
22bb101
[declare] Refactor analysis and construction of mutual lemmas
ejgallego
committed
c7a62d0
[declare] Use Recthm.t in mutual analysis functions
ejgallego
committed
e622379
[declare] Nit on regular lemma init.
ejgallego
committed
f72efb3
[vernac] Nit refatoring on lemma command interpretation
ejgallego
committed
862e5a0
[declare] Improve organization of proof/constant information.
ejgallego
committed
ea8b9e0
[declare] Improve logical code order
ejgallego
committed
bf31fad
[obligation] Switch to new declare info API.
ejgallego
committed
06159c5
[declare] Merge remaining obligations bits into Declare
ejgallego
committed
4a2c865
[declare] Remove Proof_ending from the public API
ejgallego
committed
d9dca86
[declare] Some more cleanup on unused functions after the last commits.
ejgallego
committed
4ad9fa2
[declare] Return list of declared global in Proof.save
ejgallego
committed
a5a65dd
[recLemmas] Nit on naming consistency.
ejgallego
committed
eb950df
[ci] Add overlays for PR #12372
ejgallego
committed
c62aa0e

Navigation Menu

Uh oh!

[declare] Refactor constant information into a record. - #12372

[declare] Refactor constant information into a record.#12372
SkySkimmer merged 28 commits into
rocq-prover:masterfrom
ejgallego:proof+info

Commits on Jun 26, 2020

[declare] Stronger typing for start_proof

[declare] Move proof information to declare.

[declare] Remove mutual internals from Info.t structure.

[declare] Remove Lemmas module

[declare] Refactor constant information into a record.

[declare] Make ProgramDecl.t abstract

[declare] [api] Removal of deprecated functions

[declare] [api] Removal of duplicated type aliases.

[declare] Move udecl to Info structure.

[declare] Reify Proof.t API into the Proof module.

[declare] [api] Modify logical presentation of declare interfaces

[declare] [compat] Remove exception alias.

[declare] Documentation on obligations

[declare] Nit on interface

[declare] Nit on hook call.

[declare] Refactor analysis and construction of mutual lemmas

[declare] Use Recthm.t in mutual analysis functions

[declare] Nit on regular lemma init.

[vernac] Nit refatoring on lemma command interpretation

[declare] Improve organization of proof/constant information.

[declare] Improve logical code order

[obligation] Switch to new declare info API.

[declare] Merge remaining obligations bits into Declare

[declare] Remove Proof_ending from the public API

[declare] Some more cleanup on unused functions after the last commits.

[declare] Return list of declared global in Proof.save

[recLemmas] Nit on naming consistency.

[ci] Add overlays for PR #12372