aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2019-09-16Optimize multiple importsMaxime Dénès
2019-09-16Specialize `ImportObject` to `Export`Maxime Dénès
2019-09-16Remove library-specific code for `Import`.Maxime Dénès
2019-09-04Merge PR #10612: Fix feedback levelsEmilio Jesus Gallego Arias
2019-09-02Merge PR #10562: [library] Move library to vernacMaxime Dénès
2019-09-02Merge PR #9918: Fix #9294: critical bug with template polymorphismPierre-Marie Pédrot
2019-08-30[library] Move library to vernacEmilio Jesus Gallego Arias
2019-08-29Merge PR #10674: [declare] Move proof_entry type to declare, put interactive ...Pierre-Marie Pédrot
2019-08-29Make sure that all query commands return a notice (not an info) feedbackMaxime Dénès
2019-08-27[declare] Use entry constructor instead of low-level record.Emilio Jesus Gallego Arias
2019-08-27[declare] Move proof_entry type to declare, put interactive proof data on top...Emilio Jesus Gallego Arias
2019-08-26Document `Template Check` flag and add changelog entry for 9918Matthieu Sozeau
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-08-26[glob/aux files] Remove undocumented Stdout dump, cleanup flags.Emilio Jesus Gallego Arias
2019-08-24[dune] Migrate static Dune files to Dune 1.10Emilio Jesus Gallego Arias
2019-08-23Merge PR #10665: [api] Move handling of variable implicit data to impargsGaëtan Gilbert
2019-08-20Merge PR #10291: Controlling typing flags with commands (no attribute)Gaëtan Gilbert
2019-08-19[declare] Use `binding_kind` for implicit kind instead of boolean.Emilio Jesus Gallego Arias
2019-08-19[api] Move handling of variable implicit data to impargsEmilio Jesus Gallego Arias
2019-08-16Fix Print Assumptions: Inductive types can have unsafe fixpoints orSimonBoulier
2019-08-16Universe Checking instead of Universes CheckingSimonBoulier
2019-08-16Improve [Print Assumptions] for type-in-type and assumed positive.SimonBoulier
2019-08-16Set/Unset commands for typing flagsSimonBoulier
2019-08-16Add [Print Typing Flags] command.SimonBoulier
2019-08-16Split the [check_guarded] typing_flag into [check_guarded] (for (co)fixpoints...SimonBoulier
2019-08-14[vernac] Refactor common parts of interp_{,delayed}Emilio Jesus Gallego Arias
2019-08-14[vernac] Pass control attributes to interpretation of delayed proofs.Emilio Jesus Gallego Arias
2019-08-14[vernac] Refactor Vernacular Control Attributes into a listEmilio Jesus Gallego Arias
2019-08-08Emit Feedback.AddedAxiom in Declare instead of higher layersGaëtan Gilbert
2019-08-08Merge PR #10324: Fix #10088: Ltac2 & operator conflicts with notations involv...Maxime Dénès
2019-07-31Specialize the section API.Pierre-Marie Pédrot
2019-07-29Tentatively providing a localization function to ad-hoc camlp5 parsers.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 15:28:43 +0000