aboutsummaryrefslogtreecommitdiff
path: root/vernac/vernacentries.ml
AgeCommit message (Expand)Author
2020-01-25Merge PR #11025: Add Set NativeCompute TimingMaxime Dénès
2020-01-09Merge PR #11164: [CS] allow Let variable to be canonicalPierre-Marie Pédrot
2020-01-08Add Set NativeCompute TimingJason Gross
2019-12-31Merge PR #11338: Remove uses of Global in Evd API.Gaëtan Gilbert
2019-12-28Extend `Print Canonical Projections` with a search functionalityKazuhiko Sakaguchi
2019-12-26Remove uses of Global in Evd API.Pierre-Marie Pédrot
2019-12-24[Attributes] accept #[canonical] (Let|Definition)Enrico Tassi
2019-12-22Rename files with Class in their name to make their role clearer.Pierre-Marie Pédrot
2019-12-13Use ~strict argument consistently in push_context/push_context_set intfsMatthieu Sozeau
2019-12-03Merge PR #11113: Remove deprecated compat modifier of Notation / Infix commands.Emilio Jesus Gallego Arias
2019-12-03Merge PR #11162: [CS] support #[local] attributeMaxime Dénès
2019-12-02Remove deprecated compat modifier of Notation / Infix commands.Théo Zimmermann
2019-12-02[CS] support #[local] attributeEnrico Tassi
2019-11-30Actually deprecate `SearchAbout`Maxime Dénès
2019-11-25Merge PR #11146: Combine similar arguments when printing Arguments commandHugo Herbelin
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-20make VernacArguments closer to user syntaxGaëtan Gilbert
2019-11-13Return of Refine Instance as an attribute.Gaëtan Gilbert
2019-11-13don't double parse program attribute for vernacinstanceGaëtan Gilbert
2019-11-01Merge PR #9867: Add primitive floats (binary64 floating-point numbers)Maxime Dénès
2019-11-01Implementing support for vos/vok files.charguer
2019-11-01Implement classify on primitive floatPierre Roux
2019-11-01Change return type of primitive float comparisonPierre Roux
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon
2019-11-01Declare type of primitives in CPrimitivesPierre Roux
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 02:08:42 +0000