aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-08-29Separating the module_type and module_body types by using a type parameter.Pierre-Marie Pédrot
As explained in edf85b9, the original commit that merged the module_body and module_type_body representations, this was delayed to a later time assumedly due to OCaml lack of GADTs. Actually, the only thing that was needed was polymorphic recursion, which has been around already for a relatively long time (since 3.12).
2017-08-29Post-merge API fix.Maxime Dénès
2017-08-29Merge PR #946: Functional pretyping interfaceMaxime Dénès
2017-08-29Merge PR #937: [general] Remove spurious dependency of highparsing on toplevel.Maxime Dénès
2017-08-29Merge PR #916: Fixing notation bug 5608 involving { } and a slight ↵Maxime Dénès
restructuration
2017-08-29Merge PR #838: Have coq-dpdgraph ci test print the differencesMaxime Dénès
2017-08-29Merge PR #830: Moving assert (the "Cut" rule) to new proof engineMaxime Dénès
2017-08-29Merge PR #819: Cleanup old thingsMaxime Dénès
2017-08-29Merge PR #805: Functional tacticsMaxime Dénès
2017-08-29Merge PR #773: [flags] Remove XML output flag.Maxime Dénès
2017-08-29Merge PR #966: Makefile : ignore user-contrib in various file searchesMaxime Dénès
2017-08-29Merge PR #985: Fix coqdoc test-suite target on Windows.Maxime Dénès
2017-08-29Trying to fix deployment of master on bintray, and deploy tags to github.Maxime Dénès
Deployment doesn't work on PRs, so I have to push it directly, sorry for the noise.
2017-08-29Master now deploys 8.8+alpha.Maxime Dénès
2017-08-29Quoting notations in incompatible-level error message.Hugo Herbelin
2017-08-29A new step of restructuration of notations.Hugo Herbelin
This allows to issue a more appropriate message when a notation with a { } cannot be defined because of an incompatible level. E.g.: Notation "{ A } + B" := (sumbool A B) (at level 20).
2017-08-29Adding a test for #5569 (warning about skipping spaces).Hugo Herbelin
The two previous commits make the warning irrelevant and useless.
2017-08-29Dropping former fix to bug #5469 (notation format not recognizing curly braces).Hugo Herbelin
This reverts commit 53a50875 and a bit more: it also makes the check for possibly ignoring formatting spaces irrelevant, since the previous commit makes that curly brackets are not any more dropped for printing.
2017-08-29A little reorganization of notations + a fix to #5608.Hugo Herbelin
- Formerly, notations such as "{ A } + { B }" were typically split into "{ _ }" and "_ + _". We keep the split only for parsing, which is where it is really needed, but not anymore for interpretation, nor printing. - As a consequence, one notation string can give rise to several grammar entries, but still only one printing entry. - As another consequence, "{ A } + { B }" and "A + { B }" must be reserved to be used, which is after all the natural expectation, even if the sublevels are constrained. - We also now keep the information "is ident", "is binder" in the "key" characterizing the level of a notation.
2017-08-24Update .mailmap file.Guillaume Melquiond
2017-08-21Fix coqdoc URLs under Windows.Théo Zimmermann
URLs on Windows are the same as on Unix, they use / not \.
2017-08-21Extend .gitignore for coqdoc test-suite.Théo Zimmermann
2017-08-21Fix coqdoc test-suite target on Windows.Théo Zimmermann
Commit 8f12597 introduced new output tests but these were broken on Windows. We fix them by using --strip-trailing-cr option of diff, like in other output tests in the test-suite.
2017-08-18Merge PR #965: Moving file primitive.ml to cPrimitive.ml to avoid conflict ↵Maxime Dénès
with OCaml.
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-18Separate jobs for test-suite and package building under OSX.Maxime Dénès
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 ↵Maxime Dénès
trailing / and \ on windows)
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
Only the latter is a valid git tag, and we will soon be using those to generate our version numbers.
2017-08-17Make Travis generate OSX packages.Maxime Dénès
The packages will be built only for main branches (not pull requests), and are accessible via bintray: https://bintray.com/coq/coq
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
2017-08-16Mention tclINDEPENDENTL (#349) in dev/doc/changes.Théo Zimmermann
2017-08-168.7 CHANGESThéo Zimmermann
2017-08-16change section caption, improve some wordingPaul Steckler
2017-08-16Porting #856 (8.6.1 CHANGES entries) to masterThéo Zimmermann
2017-08-16Merge PR #957: Set detachable windows type hint to dialog.Maxime Dénès
2017-08-16Merge PR #831: Port ssreflect user manual to Coq's latex/hevea styleMaxime Dénès
2017-08-16Merge PR #912: Detyping functions are now operating on EConstr.t.Maxime Dénès
2017-08-16Merge PR #942: solving b1859Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 01:46:40 +0000