aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-10-05Merge PR #1102: On the detection of evars which "advanced" (and a fix to BZ#5...Maxime Dénès
2017-10-05Merge PR #1101: Fixing an old proof engine bug in collecting evars with clear...Maxime Dénès
2017-10-05Merge PR #1059: coq_makefile: make sure compile flags for Coq and coq_makefil...Maxime Dénès
2017-10-05Merge PR #1112: Fix GeoCoq CI and remove it from allowed failuresMaxime Dénès
2017-10-05Extraction: reduce eta-redexes whose cores are atomic (solves indirectly BZ#4...Pierre Letouzey
2017-10-05Shorten the .gitattributes file.Théo Zimmermann
2017-10-05[pp] Minor optimization in `Pp.t` construction and gluing.Emilio Jesus Gallego Arias
2017-10-05[ci] Remove deploy to GitHub of OS X package.Théo Zimmermann
2017-10-05Fixing BZ#5769 (variable of type "_something" was named after invalid "_").Hugo Herbelin
2017-10-05Distinguishing pseudo-letters out of the set of unicode letters.Hugo Herbelin
2017-10-05Fixing typos in comments of unicode.ml.Hugo Herbelin
2017-10-05Fixing #5765 (an anomaly with 'pat in parameters of inductive definition).Hugo Herbelin
2017-10-05Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).Hugo Herbelin
2017-10-04Merge PR #1006: fix: ssrmatching and primitive projectionsMaxime Dénès
2017-10-04Merge PR #1078: Report missing arguments in error messageMaxime Dénès
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 23:58:44 +0000