aboutsummaryrefslogtreecommitdiff
path: root/vernac/lemmas.ml
AgeCommit message (Expand)Author
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
2019-07-23[lemmas] Refactor code a bit, saving functions now to in the saving part.Emilio Jesus Gallego Arias
2019-07-11Merge PR #10498: [api] Deprecate GlobRef constructors.Gaëtan Gilbert
2019-07-09[proof] Remove sign parameter to open_lemma.Emilio Jesus Gallego Arias
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-07-07[lemmas] Move mutually recursive lemma analysis to its own module.Emilio Jesus Gallego Arias
2019-07-03declare_variable: path is always Lib.cwd()Gaëtan Gilbert
2019-07-03Declare section variables in direct style "without" an objectGaëtan Gilbert
2019-07-01[decls] Remove goal_object_kind type.Emilio Jesus Gallego Arias
2019-07-01[declare] Separate kinds from entries in constant declarationEmilio Jesus Gallego Arias
2019-07-01[api] Refactor most of `Decl_kinds`Emilio Jesus Gallego Arias
2019-06-28Merge PR #10434: [declare] Fine tuning of Hook type.Pierre-Marie Pédrot
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-26[declare] Fine tuning of Hook type.Emilio Jesus Gallego Arias
2019-06-25[lemmas] Move `Stack` out of Lemmas.Emilio Jesus Gallego Arias
2019-06-24Use named records instead of tuples where `polymorphic` used to be.Gaëtan Gilbert
2019-06-24[proof] Move initial_euctx to proof_globalEmilio Jesus Gallego Arias
2019-06-24[proof] API Documentation fixes.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] More uniformity in proof start labels.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] Untabify.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-24Remove the export_seff flag from Declare API.Pierre-Marie Pédrot
2019-06-24Duplicate the type of constant entries in Proof_global.Pierre-Marie Pédrot
2019-06-20Merge PR #9645: [proof] Remove terminator type, unifying regular and obligati...Pierre-Marie Pédrot
2019-06-17Merge PR #10362: Kernel-side delaying of polymorphic opaque constantsGaëtan Gilbert
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-17Allow to delay polymorphic opaque constants.Pierre-Marie Pédrot
2019-06-17[equations] [proof] Remove reference to evar_mapEmilio Jesus Gallego Arias
2019-06-17[equations] [proof] Remove duplicate shrink function.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 03:38:40 +0000