aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-10-09Merge PR #1109: Handle some misc todosMaxime Dénès
2017-10-09[deps] Move `Discharge` to `interp`Emilio Jesus Gallego Arias
2017-10-09Merge PR #1086: [stm] [flags] Move document mode flags to the STM.Maxime Dénès
2017-10-09Merge PR #1062: BZ#5739, Allow level for leftmost nonterminal for printing-on...Maxime Dénès
2017-10-09Merge PR #1117: [ci] Remove temporary bignums overlay.Maxime Dénès
2017-10-09Fix Travis OSX deploy conditional.Gaëtan Gilbert
2017-10-09Include leading zeros in version infoTej Chajed
2017-10-08Changed Qeq_bool_sym into Qeq_bool_comm, used the proof of @letouzey.Raphaël Monat
2017-10-08Removed leb_not_le (already existing as Nat.leb_nle)Raphaël Monat
2017-10-07Implementing the Constr.in_context function.Pierre-Marie Pédrot
2017-10-07Remove unused warnings.Pierre-Marie Pédrot
2017-10-07Fix coq/ltac2#30: Compilation broken since -safe-string PR got merged.Pierre-Marie Pédrot
2017-10-07Revert "Switch Travis to OSX 10.12 and Xcode 8.3.3."Théo Zimmermann
2017-10-07Fix hardcoded boot dependencies after #1041.Gaëtan Gilbert
2017-10-07travis: remove the overlay on bignumsPierre Letouzey
2017-10-07Compat/Coq87.v : Unset Omega UseLocalDefs (see PR #768)Pierre Letouzey
2017-10-06[stm] Switch to a functional APIEmilio Jesus Gallego Arias
2017-10-06[stm] [flags] Move document mode flags to the STM.Emilio Jesus Gallego Arias
2017-10-06[coqtop] Don't reset coqinit internal variables after initialization.Emilio Jesus Gallego Arias
2017-10-06Merge PR #1127: Shorten the .gitattributes file.Maxime Dénès
2017-10-06Merge PR #1118: Extraction : minor support stuff for the new Extraction Compu...Maxime Dénès
2017-10-06Merge PR #1119: Fixing bug BZ#5769 (generating a name "_" out of a type "_som...Maxime Dénès
2017-10-06Merge PR #1121: Fixing BZ#5765 (an anomaly with 'pat in the parameters of an ...Maxime Dénès
2017-10-06Merge PR #1125: [pp] Minor optimization in `Pp.t` construction and gluing.Maxime Dénès
2017-10-06Merge PR #1124: Extraction: reduce atomic eta-redexes (solves indirectly BZ#4...Maxime Dénès
2017-10-06Merge PR #1128: GitLab CI: make all_stdlib.v in build jobMaxime Dénès
2017-10-06Merge PR #1130: Fix copyright info in reference manual.Maxime Dénès
2017-10-06Merge PR #1131: Clean-up xml protocol docMaxime Dénès
2017-10-06Merge PR #1129: 8.7+beta2 CHANGESMaxime Dénès
2017-10-06Merge PR #1123: [ci] Remove deploy to GitHub of OS X package.Maxime Dénès
2017-10-06TimeFileMaker.py: Allow trailing spacesJason Gross
2017-10-06Extract changes to the XML protocol from its docThéo Zimmermann
2017-10-06Make the XML protocol doc more version-independentThéo Zimmermann
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