aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* | | | | | | | | | | | | | | | | | Merge PR #1093: [doc] Update INSTALL to match reality.Gravatar Maxime Dénès2017-10-05
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1107: Add coqwc tests to test suiteGravatar Maxime Dénès2017-10-05
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | * | | | | | | | | | | | | GitLab CI: make all_stdlib.v in build jobGravatar Gaëtan Gilbert2017-10-05
| | | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | | Merge PR #1106: Fix beautifierGravatar Maxime Dénès2017-10-05
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1102: On the detection of evars which "advanced" (and a fix to ↵Gravatar Maxime Dénès2017-10-05
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BZ#5757)
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1101: Fixing an old proof engine bug in collecting evars with ↵Gravatar Maxime Dénès2017-10-05
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | cleared context.
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1059: coq_makefile: make sure compile flags for Coq and ↵Gravatar Maxime Dénès2017-10-05
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | coq_makefile are in sync (supersed #1039)…
* | | | | | | | | | | | | | | | | | | | | | | Merge PR #1112: Fix GeoCoq CI and remove it from allowed failuresGravatar Maxime Dénès2017-10-05
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | * | | | | | | | | | | | Extraction: reduce eta-redexes whose cores are atomic (solves indirectly ↵Gravatar Pierre Letouzey2017-10-05
| |_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BZ#4852) This code simplification isn't that important, but it can trigger further simplifications elsewhere, see for instance BZ#4852. NB: normally, the extraction favors eta-expanded forms, since that's the usual way to avoid issues about '_a type variables that cannot be generalized. But the atomic eta-reductions done here shouldn't be problematic (no applications put outside of functions).
| | | | | | | | | | | | | | | | * | | | | | | Shorten the .gitattributes file.Gravatar Théo Zimmermann2017-10-05
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | .dir-locals.el can be useful for users of the tarballs as well, and TODO doesn't exist anymore.
| | | | | | | | | | | | * | | | | | | | | | [pp] Minor optimization in `Pp.t` construction and gluing.Gravatar Emilio Jesus Gallego Arias2017-10-05
| |_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The typical Coq `Pp.t` document contains a lot of "gluing" which produces efficient structures but it is quite painful in serialization. We optimize a common document building case so we don't create as much glue nodes as with the "naive" strategy, and without incurring in the large performance cost full flattening would produce. This is a temporal fixup, see #505 for more context on the discussion and medium-term plans.
| | | | | | | | | | | * | | | | | | | | | [ci] Remove deploy to GitHub of OS X package.Gravatar Théo Zimmermann2017-10-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is inconvenient because it can only be tested on tags and it didn't work for V8.7+beta1.
| | | | | | | | | | | | | * | | | | | | | Fixing BZ#5769 (variable of type "_something" was named after invalid "_").Gravatar Hugo Herbelin2017-10-05
| | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | | | | | | | Distinguishing pseudo-letters out of the set of unicode letters.Gravatar Hugo Herbelin2017-10-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This includes _ and insecable space which can be used in idents and this allows more precise heuristics.
| | | | | | | | | | | | | * | | | | | | | Fixing typos in comments of unicode.ml.Gravatar Hugo Herbelin2017-10-05
| | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | * | | | | | | | | Fixing #5765 (an anomaly with 'pat in parameters of inductive definition).Gravatar Hugo Herbelin2017-10-05
| | | | | | | | | | | | |/ / / / / / / /
* | | | | | | | | | | | | | | | | | | | Merge PR #1006: fix: ssrmatching and primitive projectionsGravatar Maxime Dénès2017-10-04
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1078: Report missing arguments in error messageGravatar Maxime Dénès2017-10-04
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | * | | | | | | Extraction : minor support stuff for the new Extraction Compute pluginGravatar Pierre Letouzey2017-10-04
| | | | | | | | | | | | | | |/ / / / / / / | | | | | | | | | | | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | See https://github.com/letouzey/extraction-compute for more details
* | | | | | | | | | | | | | | | | | | | | Merge PR #1096: [stm] Warn about costly Undo operations in batch mode [BZ#5677]Gravatar Maxime Dénès2017-10-04
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | * | | | | | [ci] Remove temporary bignums overlay.Gravatar Théo Zimmermann2017-10-04
| | | | | | | | | | | | | | | |/ / / / / / | | | | | | | | | | | | | | |/| | | | | |
* | | | | | | | | | | | | | | | | | | | | Merge PR #1058: Fixing BZ#5741 (anomaly in info_trivial).Gravatar Maxime Dénès2017-10-04
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | * | | | | | | | | | | add coqwc testsGravatar Paul Steckler2017-10-03
| | | | | | | | | | | |_|_|_|/ / / / / / | | | | | | | | | | |/| | | | | | | | |
| | | | | | | | | | | | | | | | | | * | autolink to Github PRs from BugzillaGravatar Paul Steckler2017-10-03
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | * | Ltac uses the new generic locatable API.Gravatar Pierre-Marie Pédrot2017-10-03
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | * | Implementing a generic mechanism for locating named objects from Coq side.Gravatar Pierre-Marie Pédrot2017-10-03
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | * | Moving the Ltac-specific part of the nametab to the Ltac plugin.Gravatar Pierre-Marie Pédrot2017-10-03
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | For now, a few vernacular features were lot in the process, like locating Ltac definitions. This will be fixed in an upcoming commit.
| | | | | | * | | | | | | | | | | | fix compilation on OCaml < 4.04Gravatar Enrico Tassi2017-10-03
| | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | Merge PR #1110: Mention requiring extraction/funind in CHANGESGravatar Maxime Dénès2017-10-03
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1105: [stm] Remove unused "Proof using" data in `Sync` tags.Gravatar Maxime Dénès2017-10-03
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1104: Browser userscript to turn BZ#XXXX occurences into links.Gravatar Maxime Dénès2017-10-03
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1100: Avoid looping when searching for CoqProject.Gravatar Maxime Dénès2017-10-03
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1099: BZ#5637, look for Obligation num or Next Obligation to start ↵Gravatar Maxime Dénès2017-10-03
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | proof for coqwc
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1097: Properly display the "only" prefix for selectors (bug #5760).Gravatar Maxime Dénès2017-10-03
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1094: Fixing a little parsing bug with level 90 introduced in ↵Gravatar Maxime Dénès2017-10-03
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 3e70ea9c.
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1090: [ide] Avoid duplicate error printing (BZ#5583)Gravatar Maxime Dénès2017-10-03
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1084: After testing it in live, writing metas using an ↵Gravatar Maxime Dénès2017-10-03
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ?INTERNAL#42 style is ugly
| | | | | | | | | | | | | | * | | | | | | | | | | | | Remove GeoCoq from allowed failures.Gravatar Théo Zimmermann2017-10-03
| | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | * | | | | | | | | | | | | Fix GeoCoq build by using a shared CI configure.Gravatar Théo Zimmermann2017-10-03
| |_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | See also GeoCoq/GeoCoq#7.
* | | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #1015: Adding a function to be typically used to pass values from ↵Gravatar Maxime Dénès2017-10-03
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | an OCaml "when" clause to the r.h.s of the matching clause
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1080: Remove some unused parts of the reference manual.Gravatar Maxime Dénès2017-10-03
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1076: Properly handle "coq_makefile -Q . Foo" (bug #5580).Gravatar Maxime Dénès2017-10-03
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1072: Do not run Travis OS X packaging job on PRsGravatar Maxime Dénès2017-10-03
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1040: Efficient fresh name generationGravatar Maxime Dénès2017-10-03
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1023: dev/build/windows/makecoq_mingw.sh: install camlp5's META fileGravatar Maxime Dénès2017-10-03
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1019: Fix BZ#5655 by avoiding the creation of a cleaner thread for ↵Gravatar Maxime Dénès2017-10-03
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | empty queues.
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1012: Make a test for coq_makefile portable.Gravatar Maxime Dénès2017-10-03
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #667: [vernac] Remove `Qed exporting` syntax.Gravatar Maxime Dénès2017-10-03
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | * | | | | | | | | | | | | | | | Mention requiring extraction/funind in CHANGESGravatar Tej Chajed2017-10-02
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * | Remove a failwith ""Gravatar Gaëtan Gilbert2017-09-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 19:33:49 +0000