aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Canonically renaming fold_map into fold_left_map in library Name.Gravatar Hugo Herbelin2017-08-29
| | | | Also adding fold_right_map by consistency.
* Adapting code to renaming Option.fold_map -> Option.fold_left_map.Gravatar Hugo Herbelin2017-08-29
|
* Canonically renaming fold_map into fold_left_map in library Option.Gravatar Hugo Herbelin2017-08-29
| | | | Also adding fold_right_map by consistency.
* Adapting code to renaming Array.fold_map -> Array.fold_left_map.Gravatar Hugo Herbelin2017-08-29
|
* Canonically renaming fold_map into fold_left_map in library Array.Gravatar Hugo Herbelin2017-08-29
| | | | | Also renaming fold_map' into fold_right_map, and fold_map2' into fold_right2_map.
* Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_mapGravatar Hugo Herbelin2017-08-29
| | | | (from module List).
* Adding combinators + a canonical renaming in cList.ml.Gravatar Hugo Herbelin2017-08-29
| | | | | - Adding fold_left2_map/fold_right2_map. - Canonically renaming fold_map/fold_map' into fold_left_map/fold_right_map.
* Update .mailmap file.Gravatar Guillaume Melquiond2017-08-24
|
* Merge PR #965: Moving file primitive.ml to cPrimitive.ml to avoid conflict ↵Gravatar Maxime Dénès2017-08-18
|\ | | | | | | with OCaml.
* \ Merge PR #983: Correct the option for cumulativity in CHANGESGravatar Maxime Dénès2017-08-18
|\ \
* \ \ Merge PR #973: Adding documentation for Printing Focused option.Gravatar Maxime Dénès2017-08-18
|\ \ \
| | * | Correct the option for cumulativity in CHANGESGravatar Amin Timany2017-08-18
| | | |
* | | | Merge PR #801: Make Travis generate OSX packages.Gravatar Maxime Dénès2017-08-18
|\ \ \ \ | |_|/ / |/| | |
| * | | Separate jobs for test-suite and package building under OSX.Gravatar Maxime Dénès2017-08-18
| | | |
* | | | Merge PR #972: 8.7 change entriesGravatar Maxime Dénès2017-08-17
|\ \ \ \
* \ \ \ \ Merge PR #490: A possible fix for #5391 (command line tools do not accept ↵Gravatar Maxime Dénès2017-08-17
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | trailing / and \ on windows)
* \ \ \ \ \ Merge PR #974: Change section caption, improve some wordingGravatar Maxime Dénès2017-08-17
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #976: Document anonymous universes (PR #544).Gravatar Maxime Dénès2017-08-17
|\ \ \ \ \ \ \
| | | | * | | | Use the wording suggested by Gaetan.Gravatar Théo Zimmermann2017-08-17
| | | | | | | |
| | | | * | | | Addition suggested by Pierre-Marie.Gravatar Théo Zimmermann2017-08-17
| | | | | | | |
| | | | | * | | Change 8.7~alpha to 8.7+alpha.Gravatar Maxime Dénès2017-08-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Only the latter is a valid git tag, and we will soon be using those to generate our version numbers.
| | | | | * | | Make Travis generate OSX packages.Gravatar Maxime Dénès2017-08-17
| |_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | The packages will be built only for main branches (not pull requests), and are accessible via bintray: https://bintray.com/coq/coq
| * | | | | | Document anonymous universes (PR #544).Gravatar Gaëtan Gilbert2017-08-17
|/ / / / / /
| | | | * / Adding documentation for Printing Focused option.Gravatar Pierre Courtieu2017-08-17
| |_|_|/ / |/| | | |
| | | * | Additions following Hugo's suggestions.Gravatar Théo Zimmermann2017-08-16
| | | | |
| * | | | mention that tactic is the identity or gives errorGravatar Paul Steckler2017-08-16
| | | | |
| | | * | Improve wording.Gravatar Théo Zimmermann2017-08-16
| | | | |
| | | * | Mention tclINDEPENDENTL (#349) in dev/doc/changes.Gravatar Théo Zimmermann2017-08-16
| | | | |
| | | * | 8.7 CHANGESGravatar Théo Zimmermann2017-08-16
| | | | |
| * | | | change section caption, improve some wordingGravatar Paul Steckler2017-08-16
|/ / / /
| | * / Porting #856 (8.6.1 CHANGES entries) to masterGravatar Théo Zimmermann2017-08-16
| |/ / |/| |
* | | Merge PR #957: Set detachable windows type hint to dialog.Gravatar Maxime Dénès2017-08-16
|\ \ \
* \ \ \ Merge PR #831: Port ssreflect user manual to Coq's latex/hevea styleGravatar Maxime Dénès2017-08-16
|\ \ \ \
* \ \ \ \ Merge PR #912: Detyping functions are now operating on EConstr.t.Gravatar Maxime Dénès2017-08-16
|\ \ \ \ \
* \ \ \ \ \ Merge PR #942: solving b1859Gravatar Maxime Dénès2017-08-16
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #954: Print names of all open blocksGravatar Maxime Dénès2017-08-16
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #964: More portable location for the time command.Gravatar Maxime Dénès2017-08-16
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #951: Makefile: install-byte works even if -coqide noGravatar Maxime Dénès2017-08-16
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #841: Timorous fix of bug #5598 on global existing class in sectionsGravatar Maxime Dénès2017-08-16
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #948: [doc] Write (@nil nat) instead of (nil nat)Gravatar Maxime Dénès2017-08-16
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #944: Fix typos. Improve wording.Gravatar Maxime Dénès2017-08-16
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #943: Reference Manual: minor wording improvementsGravatar Maxime Dénès2017-08-16
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #940: Replace jarring use of "Remark" with "Note"Gravatar Maxime Dénès2017-08-16
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #934: Fix some coq-tex errors in the reference manual.Gravatar Maxime Dénès2017-08-16
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #880: Fix coqdoc bug #5648 on user idents colliding with keywords ↵Gravatar Maxime Dénès2017-08-16
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | wrongly tagged as keywords
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #864: Some cleanups after cumulativity for inductive typesGravatar Maxime Dénès2017-08-16
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | * | Removing trailing "/" and "\" in directory names only on win32.Gravatar Hugo Herbelin2017-08-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This refines e234f3ef. By the way, note that e234f3ef fixed #5391 (command line tools do not accept trailing "/" - or "\" - in windows).
| | | | | | | | | | | | * | | | | | Adding a test for BZ#1859 as suggested by @tchajed.Gravatar Théo Zimmermann2017-08-15
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | * Moving file primitive.ml to cPrimitive.ml to avoid conflict with OCaml.Gravatar Hugo Herbelin2017-08-12
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Indeed OCaml has a similar file and this conflicts, at least in debugger.
* | | | | | | | | | | | | | | | | Merge PR #963: fix coq_makefileGravatar Maxime Dénès2017-08-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 16:42:33 +0000