aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-10-09Merge PR #1087: [stm] Switch to a functional APIMaxime Dénès
2017-10-09Merge PR #1126: [ltac] Warning for deprecated `Add Setoid` and `Add Morphism`...Maxime Dénès
2017-10-09Merge PR #1134: Revert "Switch Travis to OSX 10.12 and Xcode 8.3.3."Maxime Dénès
2017-10-09Merge PR #1133: Fix hardcoded boot dependencies after #1041.Maxime Dénès
2017-10-09Merge PR #1132: TimeFileMaker.py: Allow trailing spacesMaxime Dénès
2017-10-09Merge PR #1115: Autolink to Github PRs from BugzillaMaxime Dénès
2017-10-09Merge PR #1114: Generic handling of nameable objects for pluginsMaxime Dénès
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-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