aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-10-04Extraction : minor support stuff for the new Extraction Compute pluginPierre Letouzey
2017-10-04Merge PR #1096: [stm] Warn about costly Undo operations in batch mode [BZ#5677]Maxime Dénès
2017-10-04[ci] Remove temporary bignums overlay.Théo Zimmermann
2017-10-04Merge PR #1058: Fixing BZ#5741 (anomaly in info_trivial).Maxime Dénès
2017-10-03add coqwc testsPaul Steckler
2017-10-03autolink to Github PRs from BugzillaPaul Steckler
2017-10-03Changed the statement of leb_not_le; shortened the proofRaphaël Monat
2017-10-03Ltac uses the new generic locatable API.Pierre-Marie Pédrot
2017-10-03Implementing a generic mechanism for locating named objects from Coq side.Pierre-Marie Pédrot
2017-10-03Moving the Ltac-specific part of the nametab to the Ltac plugin.Pierre-Marie Pédrot
2017-10-03fix compilation on OCaml < 4.04Enrico Tassi
2017-10-03Merge branch 'master' of https://github.com/coq/coqRaphaël Monat
2017-10-03Add Qabs_Qinv: Qabs (/ q) == / (Qabs q).Raphaël Monat
2017-10-03Add Qeq_bool_sym: Qeq_bool x y = Qeq_bool y x.Raphaël Monat
2017-10-03Add leb_not_le: (n <=? m) = false -> n > m.Raphaël Monat
2017-10-03Merge PR #1110: Mention requiring extraction/funind in CHANGESMaxime Dénès
2017-10-03Merge PR #1105: [stm] Remove unused "Proof using" data in `Sync` tags.Maxime Dénès
2017-10-03Merge PR #1104: Browser userscript to turn BZ#XXXX occurences into links.Maxime Dénès
2017-10-03Merge PR #1100: Avoid looping when searching for CoqProject.Maxime Dénès
2017-10-03Merge PR #1099: BZ#5637, look for Obligation num or Next Obligation to start ...Maxime Dénès
2017-10-03Merge PR #1097: Properly display the "only" prefix for selectors (bug #5760).Maxime Dénès
2017-10-03Merge PR #1094: Fixing a little parsing bug with level 90 introduced in 3e70e...Maxime Dénès
2017-10-03Merge PR #1090: [ide] Avoid duplicate error printing (BZ#5583)Maxime Dénès
2017-10-03Merge PR #1084: After testing it in live, writing metas using an ?INTERNAL#42...Maxime Dénès
2017-10-03Remove GeoCoq from allowed failures.Théo Zimmermann
2017-10-03Fix GeoCoq build by using a shared CI configure.Théo Zimmermann
2017-10-03Merge PR #1015: Adding a function to be typically used to pass values from an...Maxime Dénès
2017-10-03Merge PR #1080: Remove some unused parts of the reference manual.Maxime Dénès
2017-10-03Merge PR #1076: Properly handle "coq_makefile -Q . Foo" (bug #5580).Maxime Dénès
2017-10-03Merge PR #1072: Do not run Travis OS X packaging job on PRsMaxime Dénès
2017-10-03Merge PR #1040: Efficient fresh name generationMaxime Dénès
2017-10-03Merge PR #1023: dev/build/windows/makecoq_mingw.sh: install camlp5's META fileMaxime Dénès
2017-10-03Merge PR #1019: Fix BZ#5655 by avoiding the creation of a cleaner thread for ...Maxime Dénès
2017-10-03Merge PR #1012: Make a test for coq_makefile portable.Maxime Dénès
2017-10-03Merge PR #667: [vernac] Remove `Qed exporting` syntax.Maxime Dénès
2017-10-02Mention requiring extraction/funind in CHANGESTej Chajed
2017-09-29Remove a failwith ""Gaëtan Gilbert
2017-09-29Remove unused Failure catchGaëtan Gilbert
2017-09-29Remove TODO comment (Evar.t is opaque)Gaëtan Gilbert
2017-09-29Cleanup suggest_bulletGaëtan Gilbert
2017-09-29Typo in coqdep manGaëtan Gilbert
2017-09-29Remove some duplication between Typeops and Nativenorm.Gaëtan Gilbert
2017-09-29start counting at 0...Ralf Jung
2017-09-29[ide] Avoid duplicate error printing (BZ#5583)Emilio Jesus Gallego Arias
2017-09-29[vernac] Remove `Qed exporting` syntax.Emilio Jesus Gallego Arias
2017-09-29Iris CI: use opam to determine std++ git commitRalf Jung
2017-09-28Remove trivial TODO comment (constants can't be template poly now).Gaëtan Gilbert
2017-09-28Efficient computation of the names contained in an environment.Pierre-Marie Pédrot
2017-09-28Efficient fresh name generation relying on sets.Pierre-Marie Pédrot
2017-09-27Remove catch-all try with in the beautifier.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-19 03:49:54 +0000