aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2019-11-01Add "==", "<", "<=" in PrimFloat.vErik Martin-Dorel
2019-11-01Add next_{up,down} primitive float functionsPierre Roux
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-31Merge PR #10985: Print argument info as an Arguments command in AboutEmilio Jesus Gallego Arias
2019-10-31[prettyp] remove `mod_ops` and `indirect_accessor` parametersGaëtan Gilbert
2019-10-31Merge PR #10997: Implement the unsupported attribute error using the warning ...Emilio Jesus Gallego Arias
2019-10-31restore red behaviour printingGaëtan Gilbert
2019-10-31ppvernac: bidi hints use & not |Gaëtan Gilbert
2019-10-31Print argument info as an Arguments command in AboutGaëtan Gilbert
2019-10-31Move prettyp (Print implementation) to vernac/Gaëtan Gilbert
2019-10-31Move Arguments implementation to its own file (from vernacentries)Gaëtan Gilbert
2019-10-30Rename the 2 local type_cstr nonterminals to give them unique namesJim Fehrle
2019-10-30Implement the unsupported attribute error using the warning systemGaëtan Gilbert
2019-10-30Merge PR #10960: Move inference_hook from vernacentries to lemmasEmilio Jesus Gallego Arias
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 10:31:14 +0000