aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Omega now aware of context variables with bodies (in type Z or nat) (fix bug ...Gravatar Pierre Letouzey2017-10-05
* Merge PR #1069: Improve support for -w optionsGravatar Maxime Dénès2017-10-05
|\
* \ Merge PR #1081: Mini fix at improving the cannot unify error messageGravatar Maxime Dénès2017-10-05
|\ \
* | | Fix typo in INSTALLGravatar Maxime Dénès2017-10-05
* | | Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 t...Gravatar Maxime Dénès2017-10-05
|\ \ \
* \ \ \ 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
|\ \ \ \ \
* \ \ \ \ \ 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 BZ#5...Gravatar Maxime Dénès2017-10-05
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #1101: Fixing an old proof engine bug in collecting evars with clear...Gravatar Maxime Dénès2017-10-05
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #1059: coq_makefile: make sure compile flags for Coq and coq_makefil...Gravatar Maxime Dénès2017-10-05
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #1112: Fix GeoCoq CI and remove it from allowed failuresGravatar Maxime Dénès2017-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
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1096: [stm] Warn about costly Undo operations in batch mode [BZ#5677]Gravatar Maxime Dénès2017-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
| | | | | | * | | | | | | | | 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
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ 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 3e70e...Gravatar Maxime Dénès2017-10-03
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ 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 ?INTERNAL#42...Gravatar Maxime Dénès2017-10-03
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | * | | | | | | | | | 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
| |_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | | | | | Merge PR #1015: Adding a function to be typically used to pass values from an...Gravatar Maxime Dénès2017-10-03
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ 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
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ 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
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | * | | | | | | | | | | | | | | | | | | [ide] Avoid duplicate error printing (BZ#5583)Gravatar Emilio Jesus Gallego Arias2017-09-29
| * | | | | | | | | | | | | | | | | | | | | | | | | | | | | [vernac] Remove `Qed exporting` syntax.Gravatar Emilio Jesus Gallego Arias2017-09-29
|/ / / / / / / / / / / / / / / / / / / / / / / / / / / / /
| | | | * | | | | | | | | | | | | | | | | | | | | | | | | Efficient computation of the names contained in an environment.Gravatar Pierre-Marie Pédrot2017-09-28
| | | | * | | | | | | | | | | | | | | | | | | | | | | | | Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
| |_|_|/ / / / / / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | * | | | | Remove catch-all try with in the beautifier.Gravatar Théo Zimmermann2017-09-27
| | | | | | | | | | | | | | | | | | | | | | | * | | | | Beautifier gets its own formatter: fixes BZ#5704.Gravatar Théo Zimmermann2017-09-27
| | | | | | | | | | | | | | | | | * | | | | | | | | | | [stm] Warn about costly Undo operations in batch mode [BZ#5677]Gravatar Emilio Jesus Gallego Arias2017-09-27
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | * | | | | | | | | | | | [stm] Remove unused "Proof using" data in `Sync` tags.Gravatar Emilio Jesus Gallego Arias2017-09-27
| |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | * | | | | | | | | | | | Browser userscript to turn BZ#XXXX occurences into links.Gravatar Gaëtan Gilbert2017-09-27
| |_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | | | | | | | | | | | Avoid looping when searching for CoqProject.Gravatar Maxime Dénès2017-09-27
| |_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | * | | | | | Moving setting of "cleared" evar flag directly in Evd.restrict.Gravatar Hugo Herbelin2017-09-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-25 05:25:59 +0000