aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2019-07-29Merge PR #10574: Remove deprecated `Backtrack` commandEnrico Tassi
2019-07-29Merge PR #10538: [vernac] [inductive] Remove unused functions/exports.Pierre-Marie Pédrot
2019-07-25Remove deprecated `Backtrack` commandMaxime Dénès
2019-07-24Merge PR #10549: [lemmas] Small cleanupsGaëtan Gilbert
2019-07-23[obligations] Use already existing type alias.Emilio Jesus Gallego Arias
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-23[vernacexpr] Remove duplicate fixpoint record.Emilio Jesus Gallego Arias
2019-07-23[vernacexpr] Refactor fixpoint AST.Emilio Jesus Gallego Arias
2019-07-19[vernac] [inductive] Remove unused functions/exports.Emilio Jesus Gallego Arias
2019-07-18Polymorphism attribute on section sets the option locally.Pierre-Marie Pédrot
2019-07-18Attach the universe polymorphic status to sections.Pierre-Marie Pédrot
2019-07-11Merge PR #10498: [api] Deprecate GlobRef constructors.Gaëtan Gilbert
2019-07-10Merge PR #10446: [proof] Remove sign parameter to open_lemma.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-08[core] [api] Support OCaml 4.08Emilio Jesus Gallego Arias
2019-07-08Merge PR #10497: [lemmas] Move mutually recursive lemma analysis to its own m...Gaëtan Gilbert
2019-07-07[lemmas] Move mutually recursive lemma analysis to its own module.Emilio Jesus Gallego Arias
2019-07-07[error] Remove special error printing pre-processingEmilio 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-03Search: do not use libobject to find variablesGaëtan Gilbert
2019-07-03Merge PR #10442: Reify libobject containersEmilio Jesus Gallego Arias
2019-07-03[vernac] Fix bad merge which resulted in wrong module name.Emilio Jesus Gallego Arias
2019-07-03Merge PR #10338: Fix #9455: avoid update_global_env when unchanged Global.uni...Emilio Jesus Gallego Arias
2019-07-03Merge PR #10419: [api] Refactor most of `Decl_kinds`Gaëtan Gilbert
2019-07-02[declare] Cleanup on imports, move exception.Emilio Jesus Gallego Arias
2019-07-02Merge PR #10340: [vernac] Remove special status of Load, turn it into VtNoProofGaëtan Gilbert
2019-07-01[decls] Remove goal_object_kind type.Emilio Jesus Gallego Arias
2019-07-01[api] Reduce declare_kinds even more.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-07-01Merge PR #10433: [vernac] Cleanup on interface of VernacentriesGaëtan Gilbert
2019-06-28Merge PR #10434: [declare] Fine tuning of Hook type.Pierre-Marie Pédrot
2019-06-28Reify libobject containersMaxime Dénès
2019-06-27[vernac] Cleanup on interface of VernacentriesEmilio Jesus Gallego Arias
2019-06-27[vernac] Remove special status of Load, turn it into VtNoProofEmilio 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-26Merge PR #9855: [Fail] Simplify `Fail` implementation.Gaëtan Gilbert
2019-06-26Merge PR #10351: [lemmas] Move `Stack` out of Lemmas.Gaëtan Gilbert
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-25Move the internal_flag type from Declare to Ind_tables.Pierre-Marie Pédrot
2019-06-25Remove the internal_flag argument from Declare API.Pierre-Marie Pédrot
2019-06-25Merge PR #10316: [lemmas] Reify info for implicits, universe decls, and rec t...Pierre-Marie Pédrot
2019-06-25Merge PR #10284: Expose set interface to option tablesPierre-Marie Pédrot
2019-06-24[proof] Remove last case of optional `?poly` arguments.Emilio Jesus Gallego Arias
2019-06-24Use named records instead of tuples where `polymorphic` used to be.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 16:44:08 +0000