aboutsummaryrefslogtreecommitdiff
path: root/vernac/lemmas.ml
AgeCommit message (Expand)Author
2020-06-26[declare] Remove Lemmas moduleEmilio Jesus Gallego Arias
2020-06-26[declare] Remove mutual internals from Info.t structure.Emilio Jesus Gallego Arias
2020-06-26[declare] Move proof information to declare.Emilio Jesus Gallego Arias
2020-06-26[declare] Stronger typing for start_proofEmilio Jesus Gallego Arias
2020-05-18[declare] Grand unification of the proof save path.Emilio Jesus Gallego Arias
2020-05-18[declare] Merge `DeclareObl` into `Declare`Emilio Jesus Gallego Arias
2020-05-18[obligations] Pre-functionalize Program stateEmilio Jesus Gallego Arias
2020-05-07[declare] Merge DeclareDef into DeclareEmilio Jesus Gallego Arias
2020-04-15[declare] Rename `Declare.t` to `Declare.Proof.t`Emilio Jesus Gallego Arias
2020-04-15[proof] Merge `Proof_global` into `Declare`Emilio Jesus Gallego Arias
2020-04-15[proof] Move proof_global functionality to Proof_global from PfeditEmilio Jesus Gallego Arias
2020-03-31[proof] Split delayed and regular proof closing functions, part IIEmilio Jesus Gallego Arias
2020-03-30[declare] Fuse prepare and declare for the non-interactive path.Emilio Jesus Gallego Arias
2020-03-30[lemmas] Minor tweak to Equations API.Emilio Jesus Gallego Arias
2020-03-30[declareDef] More consistent handling of universe bindersEmilio Jesus Gallego Arias
2020-03-30[declare] Make the type of closed entries opaque.Emilio Jesus Gallego Arias
2020-03-30[lemmas] Cleanup in handling of mutual definitionsEmilio Jesus Gallego Arias
2020-03-30[lemmas] Remove workaround for non-uniform mutual bodyEmilio Jesus Gallego Arias
2020-03-30[lemmas] [internal] Reify handling of mutual assumptionsEmilio Jesus Gallego Arias
2020-03-30[proof] Miscellaneous cleanup on proof info handlingEmilio Jesus Gallego Arias
2020-03-30[lemma] Remove special case for first constant in mutual definition save path.Emilio Jesus Gallego Arias
2020-03-25[lemmas] Use direct-style for mutual lemma declaration.Emilio Jesus Gallego Arias
2020-03-25[lemmas] Use direct-style for variable declaration.Emilio Jesus Gallego Arias
2020-03-25[proof] [mutual] Factorize mutual per-entry informationEmilio Jesus Gallego Arias
2020-03-19[proof] Remove duplicated poly field in Proof_global.tEmilio Jesus Gallego Arias
2020-03-19[declare] Remaining bits on the consistency of UState.t namingEmilio Jesus Gallego Arias
2020-03-19[comFixpoing] Refactor hybrid interactive command modalityEmilio Jesus Gallego Arias
2020-03-19[declare] Bring more consistency to parameters using labelsEmilio Jesus Gallego Arias
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-13[lemmas] Consolidate some declaration data on Info.tEmilio Jesus Gallego Arias
2020-03-12[lemmas] Handle mutual lemmas more uniformly.Emilio Jesus Gallego Arias
2020-03-12[save proof] Declare universe_binders unconditionally for mutual assumptions.Emilio Jesus Gallego Arias
2020-03-12[proof] Remove duplication in the proof save path.Emilio Jesus Gallego Arias
2020-03-03[exninfo] Deprecate aliases for exception re-raising.Emilio Jesus Gallego Arias
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2019-11-08Make [Proof_global.closed_proof_output] opaqueGaëtan Gilbert
2019-10-30Merge PR #10960: Move inference_hook from vernacentries to lemmasEmilio Jesus Gallego Arias
2019-10-30Merge PR #10973: Remove dead code in save_remaining_recthmsEmilio Jesus Gallego Arias
2019-10-30Move start_proof_com from lemmas to vernacentriesGaëtan Gilbert
2019-10-29[declare] Use helper function for `fix_exn` instead of relying on internals.Emilio Jesus Gallego Arias
2019-10-29[declare] Make `proof_entry` a private type.Emilio Jesus Gallego Arias
2019-10-26Remove dead code in save_remaining_recthmsGaëtan Gilbert
2019-10-24[declare] Split universe declaration code to vernac/Emilio Jesus Gallego Arias
2019-10-13Merge PR #10670: ComAssumption cleanupPierre-Marie Pédrot
2019-10-05Declare universes for variables outside of Declare.declare_variableGaëtan Gilbert
2019-10-04Remove redundancy in section hypotheses of kernel entries.Pierre-Marie Pédrot
2019-08-27[declare] Move proof_entry type to declare, put interactive proof data on top...Emilio Jesus Gallego Arias
2019-08-19[declare] Use `binding_kind` for implicit kind instead of boolean.Emilio Jesus Gallego Arias
2019-08-08Emit Feedback.AddedAxiom in Declare instead of higher layersGaëtan Gilbert
2019-07-23[lemmas] save_remaining_recthms doesn't need a norm parameter.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-16 18:17:36 +0000