aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-08-29Quoting notations in incompatible-level error message.Hugo Herbelin
2017-08-29A new step of restructuration of notations.Hugo Herbelin
2017-08-29Adding a test for #5569 (warning about skipping spaces).Hugo Herbelin
2017-08-29Dropping former fix to bug #5469 (notation format not recognizing curly braces).Hugo Herbelin
2017-08-29A little reorganization of notations + a fix to #5608.Hugo Herbelin
2017-08-29Canonically renaming fold_map into fold_left_map in library Name.Hugo Herbelin
2017-08-29Adapting code to renaming Option.fold_map -> Option.fold_left_map.Hugo Herbelin
2017-08-29Canonically renaming fold_map into fold_left_map in library Option.Hugo Herbelin
2017-08-29Adapting code to renaming Array.fold_map -> Array.fold_left_map.Hugo Herbelin
2017-08-29Canonically renaming fold_map into fold_left_map in library Array.Hugo Herbelin
2017-08-29Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_mapHugo Herbelin
2017-08-29Adding combinators + a canonical renaming in cList.ml.Hugo Herbelin
2017-08-25primproj: fix bug 5245, hnf on proj with simpl never flag.Matthieu Sozeau
2017-08-24[ci] [gitlab] coq-dpdgraph: Remove allow-failureJason Gross
2017-08-24Program: fix BZ#5683, missing lift when building case predicateMatthieu Sozeau
2017-08-24Update .mailmap file.Guillaume Melquiond
2017-08-23Update coypright dates on documentationMatthieu Sozeau
2017-08-23Fix BZ#5687: Coqtop died badly modal message box from CoqIDE.Pierre-Marie Pédrot
2017-08-22use OCaml 4.03-compatible Filename functionsPaul Steckler
2017-08-22Prevent overallocation in Array.map_to_list and remove custom implementation ...Guillaume Melquiond
2017-08-22Fix obsolete description of real numerals.Guillaume Melquiond
2017-08-21Fix coqdoc URLs under Windows.Théo Zimmermann
2017-08-21Extend .gitignore for coqdoc test-suite.Théo Zimmermann
2017-08-21Fix coqdoc test-suite target on Windows.Théo Zimmermann
2017-08-18use OCaml temp_file, instead of our own versionPaul Steckler
2017-08-18add CHANGES entryPaul Steckler
2017-08-18move filename search to start_profilerPaul Steckler
2017-08-18Merge PR #965: Moving file primitive.ml to cPrimitive.ml to avoid conflict wi...Maxime Dénès
2017-08-18Merge PR #983: Correct the option for cumulativity in CHANGESMaxime Dénès
2017-08-18Merge PR #973: Adding documentation for Printing Focused option.Maxime Dénès
2017-08-18Correct the option for cumulativity in CHANGESAmin Timany
2017-08-18Merge PR #801: Make Travis generate OSX packages.Maxime Dénès
2017-08-18Don't belittle the size of the SE communityTej Chajed
2017-08-18Separate jobs for test-suite and package building under OSX.Maxime Dénès
2017-08-18Don't mention coq-club at allTej Chajed
2017-08-18Advise contributors to use SE over coq-clubTej Chajed
2017-08-17Add native compute profiling, BZ#5170Paul Steckler
2017-08-17Merge PR #972: 8.7 change entriesMaxime Dénès
2017-08-17Merge PR #490: A possible fix for #5391 (command line tools do not accept tra...Maxime Dénès
2017-08-17Merge PR #974: Change section caption, improve some wordingMaxime Dénès
2017-08-17Merge PR #976: Document anonymous universes (PR #544).Maxime Dénès
2017-08-17Use the wording suggested by Gaetan.Théo Zimmermann
2017-08-17Addition suggested by Pierre-Marie.Théo Zimmermann
2017-08-17Change 8.7~alpha to 8.7+alpha.Maxime Dénès
2017-08-17Make Travis generate OSX packages.Maxime Dénès
2017-08-17Document anonymous universes (PR #544).Gaëtan Gilbert
2017-08-17Adding documentation for Printing Focused option.Pierre Courtieu
2017-08-16Additions following Hugo's suggestions.Théo Zimmermann
2017-08-16mention that tactic is the identity or gives errorPaul Steckler
2017-08-16Improve wording.Théo Zimmermann