aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-10-06Fix copyright info in reference manual.Théo Zimmermann
2017-10-068.7+beta2 CHANGESThéo Zimmermann
2017-10-05[ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.Emilio Jesus Gallego Arias
2017-10-05romega: takes advantage of context variables with bodyPierre Letouzey
2017-10-05Omega now aware of context variables with bodies (in type Z or nat) (fix bug ...Pierre Letouzey
2017-10-05Merge PR #1069: Improve support for -w optionsMaxime Dénès
2017-10-05Merge PR #1081: Mini fix at improving the cannot unify error messageMaxime Dénès
2017-10-05Fix typo in INSTALLMaxime Dénès
2017-10-05Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 t...Maxime Dénès
2017-10-05Merge PR #1093: [doc] Update INSTALL to match reality.Maxime Dénès
2017-10-05Merge PR #1107: Add coqwc tests to test suiteMaxime Dénès
2017-10-05GitLab CI: make all_stdlib.v in build jobGaëtan Gilbert
2017-10-05Merge PR #1106: Fix beautifierMaxime Dénès
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-13 23:09:03 +0000