aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2019-11-27[release] Update files for 8.12 release per release process.Emilio Jesus Gallego Arias
2019-11-26indTyping: error instead of anomaly for ill-formed templateGaëtan Gilbert
2019-11-26Fix #11039: proof of False with template poly and nonlinear universesGaëtan Gilbert
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-21Merge PR #11103: Grammars: unification fix/cofix between constr/vernac + clea...Emilio Jesus Gallego Arias
2019-11-21Merge PR #11075: load .vo when .vos is missing + misc vos changesEmilio Jesus Gallego Arias
2019-11-20Combine similar arguments when printing Arguments commandGaëtan Gilbert
2019-11-20make VernacArguments closer to user syntaxGaëtan Gilbert
2019-11-20From CoqIDE or -vos or -vok compilation, load .vo when .vos is missing (fixin...charguer
2019-11-19G_constr: Renaming record_fields_instance -> fields_def.Hugo Herbelin
2019-11-19Grammar: mini-factorization between fix/cofix and Fixpoint/CoFixpoint.Hugo Herbelin
2019-11-16Merge PR #10996: Refine Instance returnsPierre-Marie Pédrot
2019-11-15Merge PR #11079: Rename non-unique local nonterminalsHugo Herbelin
2019-11-14Rename non-unique local nonterminalsJim Fehrle
2019-11-13cleanup unused argument for Classes.do_instance_resolve_TCGaë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-12Merge PR #11045: Forbid Include inside sectionsPierre-Marie Pédrot
2019-11-11Run update-compat script with --release option.Théo Zimmermann
2019-11-11Merge PR #11052: Fix #11048: uncaught destKO in inductive typePierre-Marie Pédrot
2019-11-08Make [Proof_global.closed_proof_output] opaqueGaëtan Gilbert
2019-11-05Fix #11048: uncaught destKO in inductive typeGaëtan Gilbert
2019-11-05Forbid Include inside sectionsGaëtan Gilbert
2019-11-02Merge PR #11007: [classes] Some refactoring on proof save preparation.Gaëtan Gilbert
2019-11-01Merge PR #10647: Expose universe processing in comInductive.Gaëtan Gilbert
2019-11-01Merge PR #9867: Add primitive floats (binary64 floating-point numbers)Maxime Dénès
2019-11-01minor cleanup of anonymous functionsGaëtan Gilbert
2019-11-01Expose universe processing in comInductive.Jan-Oliver Kaiser
2019-11-01Implementing support for vos/vok files.charguer
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-31[classes] Remove a couple of unneeded option typesEmilio Jesus Gallego Arias
2019-10-31[classes] Untabify in preparation for next commit.Emilio Jesus Gallego Arias
2019-10-31[classes] Some refactoring on proof save preparation.Emilio Jesus Gallego Arias
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 18:20:15 +0000