aboutsummaryrefslogtreecommitdiff
path: root/vernac/vernacentries.ml
AgeCommit message (Expand)Author
2019-10-31[prettyp] remove `mod_ops` and `indirect_accessor` parametersGaëtan Gilbert
2019-10-31Move Arguments implementation to its own file (from vernacentries)Gaëtan Gilbert
2019-10-30Move start_proof_com from lemmas to vernacentriesGaëtan Gilbert
2019-10-24[declare] Split universe declaration code to vernac/Emilio Jesus Gallego Arias
2019-10-14Use kernel info from Global for Lib.sections_{depth,are_opened}Gaëtan Gilbert
2019-10-13Merge PR #10670: ComAssumption cleanupPierre-Marie Pédrot
2019-10-07[vernac] Split vernacular translation and interpretation.Emilio Jesus Gallego Arias
2019-10-05Move do_primitive from comassumption to its own module.Gaëtan Gilbert
2019-10-04Merge PR #10798: Loosen restrictions on mixing universe mono/polymorphism in ...Pierre-Marie Pédrot
2019-10-02Loosen restrictions on mixing universe mono/polymorphism in sectionsGaëtan Gilbert
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-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-08-30[library] Move library to vernacEmilio Jesus Gallego Arias
2019-08-29Make sure that all query commands return a notice (not an info) feedbackMaxime Dénès
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-08-20Merge PR #10291: Controlling typing flags with commands (no attribute)Gaëtan Gilbert
2019-08-16Universe Checking instead of Universes CheckingSimonBoulier
2019-08-16Set/Unset commands for typing flagsSimonBoulier
2019-08-16Add [Print Typing Flags] command.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-07-25Remove deprecated `Backtrack` commandMaxime Dénès
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-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-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-07-07[error] Remove special error printing pre-processingEmilio 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-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[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-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-26[declare] Fine tuning of Hook type.Emilio Jesus Gallego Arias
2019-06-25[lemmas] Move `Stack` out of Lemmas.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 15:17:22 +0000