aboutsummaryrefslogtreecommitdiff
path: root/vernac/lemmas.mli
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-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-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-03-30[lemmas] Minor tweak to Equations API.Emilio 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[proof] [mutual] Factorize mutual per-entry informationEmilio Jesus Gallego Arias
2020-03-19[comFixpoing] Refactor hybrid interactive command modalityEmilio Jesus Gallego Arias
2020-03-19[lemmas] Fix comment on public APIEmilio Jesus Gallego Arias
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-12[lemmas] Handle mutual lemmas more uniformly.Emilio Jesus Gallego Arias
2019-10-30Move start_proof_com from lemmas to vernacentriesGaëtan Gilbert
2019-07-09[proof] Remove sign parameter to open_lemma.Emilio Jesus Gallego Arias
2019-07-07[lemmas] Move mutually recursive lemma analysis to its own module.Emilio Jesus Gallego Arias
2019-07-01[decls] Remove goal_object_kind type.Emilio Jesus Gallego Arias
2019-07-01[api] Refactor most of `Decl_kinds`Emilio Jesus Gallego Arias
2019-06-26[proof] finalize_proof doesn't need opaque (it's already in entries)Gaëtan Gilbert
2019-06-26[stm] [vernac] Remove special ?proof parameter from vernac main pathEmilio Jesus Gallego Arias
2019-06-25[lemmas] Move `Stack` out of Lemmas.Emilio Jesus Gallego Arias
2019-06-24[api] Move `locality` from `library` to `vernac`.Emilio Jesus Gallego Arias
2019-06-24[lemmas] [proof] Split proof kinds into per-layer components.Emilio Jesus Gallego Arias
2019-06-24[proof] Remove duplicated universe polymorphic from decl_kindsEmilio Jesus Gallego Arias
2019-06-24[proof] Remove redundant universe declaration information.Emilio Jesus Gallego Arias
2019-06-24[lemmas] Turn Lemmas.info into a proper type with constructor.Emilio Jesus Gallego Arias
2019-06-24[lemmas] Reify proof information for recursive theorems.Emilio Jesus Gallego Arias
2019-06-24[lemmas] Reify info for implicits, univ_decls, prepare for rec_thms.Emilio Jesus Gallego Arias
2019-06-20Merge PR #9645: [proof] Remove terminator type, unifying regular and obligati...Pierre-Marie Pédrot
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-17[proof] Add proof save path for equations.Emilio Jesus Gallego Arias
2019-06-17[proof] Remove terminator type, unifying regular and obligation ones.Emilio Jesus Gallego Arias
2019-06-17[proof] Move declaration hooks to DeclareDef.Emilio Jesus Gallego Arias
2019-06-17[proof] drop parameter from terminator typeEmilio Jesus Gallego Arias
2019-06-17[proofs] Store hooks in the proof object.Emilio Jesus Gallego Arias
2019-06-16Adding location in warning telling implicit arguments differ in term and type.Hugo Herbelin
2019-06-09[proof] Uniformize Proof_global APIEmilio Jesus Gallego Arias
2019-06-09[save_proof] Make terminator API internal.Emilio Jesus Gallego Arias
2019-06-09[proof] Move proofs that have an associated constant to `Lemmas`Emilio Jesus Gallego Arias
2019-06-04[vernac] Interpret regular vernacs symbolicallyEmilio Jesus Gallego Arias
2019-06-04Rename Proof_global.{pstate -> t}Gaëtan Gilbert
2019-06-04Rename Proof_global.{t -> stack}Gaëtan Gilbert
2019-06-04Proof_global: pass only 1 pstate when we don't want the proof stackGaëtan Gilbert
2019-03-27[vernac] Allow path for `save_proof` where no proof state is present.Emilio Jesus Gallego Arias
2019-03-27[vernac] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-02-23[vernac] Unify declaration hooks.Emilio Jesus Gallego Arias
2019-02-05Make Program a regular attributeMaxime Dénès
2018-11-30[vernac] [hooks] Refactor towards optional hooks.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 08:05:11 +0000