aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2019-10-30Merge PR #10973: Remove dead code in save_remaining_recthmsEmilio Jesus Gallego Arias
2019-10-30Merge PR #10303: Raise an anomaly when looking up unknown constant/inductivePierre-Marie Pédrot
2019-10-30Merge PR #10949: [declare] Provide helper for private constant inlining.Pierre-Marie Pédrot
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-28[declare] Provide helper for private constant inlining.Emilio Jesus Gallego Arias
2019-10-28Merge PR #10950: [declare] Split universe and inductive declaration code to v...Gaëtan Gilbert
2019-10-28Merge PR #10952: [library] [nit] Remove unnecessary type alias.Gaëtan Gilbert
2019-10-26Remove dead code in save_remaining_recthmsGaëtan Gilbert
2019-10-25[declare] Generalize kind type on declareDefEmilio Jesus Gallego Arias
2019-10-25[vernac] [inductive] Remove unused internal export.Emilio Jesus Gallego Arias
2019-10-25[inductive] [declare] Move full inductive declaration to declareIndEmilio Jesus Gallego Arias
2019-10-24[declare] Split inductive declaration code to vernac/Emilio Jesus Gallego Arias
2019-10-24[declare] Split universe declaration code to vernac/Emilio Jesus Gallego Arias
2019-10-24[library] [nit] Remove unnecessary type alias.Emilio Jesus Gallego Arias
2019-10-24Raise an anomaly when looking up unknown constant/inductiveGaëtan Gilbert
2019-10-14Remove obj_sec field of Nametab.obj_prefix record.Gaëtan Gilbert
2019-10-14Use kernel info from Global for Lib.sections_{depth,are_opened}Gaëtan Gilbert
2019-10-13Fix #10888: Context import behaviour in modtypeGaëtan Gilbert
2019-10-13Merge PR #10670: ComAssumption cleanupPierre-Marie Pédrot
2019-10-11Merge PR #10697: [vernac] Split vernacular translation and interpretation.Gaëtan Gilbert
2019-10-11Merge PR #10844: Bump version number to 8.11.Théo Zimmermann
2019-10-07Call to update-compat.py.Pierre-Marie Pédrot
2019-10-07[vernac] Split vernacular translation and interpretation.Emilio Jesus Gallego Arias
2019-10-05Fix #10669 incorrect substitution in context outside sectionGaëtan Gilbert
2019-10-05Cleanup ComAssumptionGaëtan Gilbert
2019-10-05Move do_primitive from comassumption to its own module.Gaëtan Gilbert
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-10-04Merge PR #10798: Loosen restrictions on mixing universe mono/polymorphism in ...Pierre-Marie Pédrot
2019-10-03Merge PR #10727: [library] Move `Declaremods` to `vernac/`Pierre-Marie Pédrot
2019-10-02Loosen restrictions on mixing universe mono/polymorphism in sectionsGaëtan Gilbert
2019-09-29Merge PR #10673: [lemmas] Cleanup users of default proof information.Pierre-Marie Pédrot
2019-09-24Merge PR #10758: Fix #10757: Program Fixpoint uses "exists" for telescopesMatthieu Sozeau
2019-09-18[declaremods] Remove abstraction layer over module interpretation.Emilio Jesus Gallego Arias
2019-09-18[library] Move `Declaremods` to `vernac/`Emilio Jesus Gallego Arias
2019-09-16Fix #10757: Program Fixpoint uses "exists" for telescopesGaëtan Gilbert
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 20:02:13 +0000