aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-03-18[ci] [docker] Update to 4.09.1Emilio Jesus Gallego Arias
2020-03-18Merge PR #11607: Hide binder type in Ltac2Jason Gross
2020-03-18Adding a round-trip test for binders.Pierre-Marie Pédrot
2020-03-18Actually use the binder type for Ltac2 that should be used in the kernel.Pierre-Marie Pédrot
2020-03-18Hide the Ltac2 binder type.Pierre-Marie Pédrot
2020-03-18Rename Retypeops -> RelevanceopsGaëtan Gilbert
2020-03-18Merge PR #11559: Remove year in headers.Hugo Herbelin
2020-03-18Merge PR #11812: Add an Export locality to hintsThéo Zimmermann
2020-03-18Merge PR #11839: Dead code in g_prim.mlgPierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-18Adding overlays.Pierre-Marie Pédrot
2020-03-18Add documentation for the export hint.Pierre-Marie Pédrot
2020-03-18Export the user-facing attribute for hint locality.Pierre-Marie Pédrot
2020-03-18Also show unchanged headers.Théo Zimmermann
2020-03-18Remove dates in headers.Théo Zimmermann
2020-03-18Use a 3-valued flag for hint locality.Pierre-Marie Pédrot
2020-03-18Hack a non-superglobal mode for hints.Pierre-Marie Pédrot
2020-03-18Change some ouput tests due to the printing of implicitsSimonBoulier
2020-03-18Merge PR #11746: Register commonly used names from the Reals library for plug...Théo Zimmermann
2020-03-17Properly thread let-bindings in Funind principle construction.Pierre-Marie Pédrot
2020-03-17Merge PR #11699: Comment difference between the 2 hashes on constrPierre-Marie Pédrot
2020-03-17Merge PR #11825: [ci] [docker] Update components in Docker imageGaëtan Gilbert
2020-03-17Merge PR #11811: Remove a positivity check when Positivity Checking is offGaëtan Gilbert
2020-03-17Add test for PR11811 (disable a positivity check)SimonBoulier
2020-03-17Dead code in g_prim.mlgHugo Herbelin
2020-03-16[ci] Cleanup old overlays.Emilio Jesus Gallego Arias
2020-03-16[ci] [docker] Update components in Docker imageEmilio Jesus Gallego Arias
2020-03-16Merge PR #11813: Fixed link to "match" syntax figures.Théo Zimmermann
2020-03-16Merge PR #11831: [ci] Re-enable VST testingGaëtan Gilbert
2020-03-16Document coq_makefile behavior wrt -native-compiler yesPierre Roux
2020-03-16Fix coq-makefile/native1 testPierre Roux
2020-03-15[ci] Re-enable VST testingEmilio Jesus Gallego Arias
2020-03-15Use quotes when "necessary" in the coqtop argument window.Hugo Herbelin
2020-03-15Adding a function to encode/decode string list into a single string.Hugo Herbelin
2020-03-14Fixes #11692 (clear dependent knows about let-in).Hugo Herbelin
2020-03-14Merge PR #10858: Implementing postponed constraints in TC resolutionGaëtan Gilbert
2020-03-13Merge PR #11797: Dune build rules for doc_grammar and fullGrammar.Emilio Jesus Gallego Arias
2020-03-13Merge PR #11688: When parsing a negative integer, ensure that the minus sign ...Emilio Jesus Gallego Arias
2020-03-13Merge PR #11803: Update Azure MacOS version 10.13 -> 10.14Emilio Jesus Gallego Arias
2020-03-13[funind] [cleanup] Remove unused function parametersEmilio Jesus Gallego Arias
2020-03-13Implementing postponed constraints in TC resolutionMatthieu Sozeau
2020-03-13Update Azure MacOS version 10.13 -> 10.14Gaëtan Gilbert
2020-03-13Merge PR #11805: Fix coqchk for primitive integers on 32bit arch with OCaml >...Pierre-Marie Pédrot
2020-03-13Merge PR #11016: [proof] Remove duplication in the proof save path.Gaëtan Gilbert
2020-03-13Merge PR #11804: [CI] test hierarchy builder as part of elpiGaëtan Gilbert
2020-03-13Merge PR #11815: [ci] [doc] Point to actual docker instructions.Gaëtan Gilbert
2020-03-13Merge PR #11003: [vernac] Remove deprecated function.Gaëtan Gilbert
2020-03-13[cleanup] Remove unnecessary Map/Set module creationEmilio Jesus Gallego Arias
2020-03-13Fixing a non-protected try-with in class_tactics.ml.Hugo Herbelin
2020-03-13Double-checking at tclZERO entry that the exception is non critical.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 06:48:10 +0000