Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Merge PR #1107: Add coqwc tests to test suite | 2017-10-05 | |
|\ | |||
* \ | Merge PR #1106: Fix beautifier | 2017-10-05 | |
|\ \ | |||
* \ \ | Merge PR #1102: On the detection of evars which "advanced" (and a fix to BZ#5... | 2017-10-05 | |
|\ \ \ | |||
* \ \ \ | Merge PR #1101: Fixing an old proof engine bug in collecting evars with clear... | 2017-10-05 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #1059: coq_makefile: make sure compile flags for Coq and coq_makefil... | 2017-10-05 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #1112: Fix GeoCoq CI and remove it from allowed failures | 2017-10-05 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #1006: fix: ssrmatching and primitive projections | 2017-10-04 | |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR #1078: Report missing arguments in error message | 2017-10-04 | |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #1096: [stm] Warn about costly Undo operations in batch mode [BZ#5677] | 2017-10-04 | |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR #1058: Fixing BZ#5741 (anomaly in info_trivial). | 2017-10-04 | |
|\ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | * | add coqwc tests | 2017-10-03 | |
| | | | | | * | | | | | fix compilation on OCaml < 4.04 | 2017-10-03 | |
* | | | | | | | | | | | Merge PR #1110: Mention requiring extraction/funind in CHANGES | 2017-10-03 | |
|\ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1105: [stm] Remove unused "Proof using" data in `Sync` tags. | 2017-10-03 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1104: Browser userscript to turn BZ#XXXX occurences into links. | 2017-10-03 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1100: Avoid looping when searching for CoqProject. | 2017-10-03 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1099: BZ#5637, look for Obligation num or Next Obligation to start ... | 2017-10-03 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1097: Properly display the "only" prefix for selectors (bug #5760). | 2017-10-03 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1094: Fixing a little parsing bug with level 90 introduced in 3e70e... | 2017-10-03 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1090: [ide] Avoid duplicate error printing (BZ#5583) | 2017-10-03 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1084: After testing it in live, writing metas using an ?INTERNAL#42... | 2017-10-03 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | | | | | * | | | | | | Remove GeoCoq from allowed failures. | 2017-10-03 | |
| | | | | | | | | | | | | | * | | | | | | Fix GeoCoq build by using a shared CI configure. | 2017-10-03 | |
| |_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | | | |||
* | | | | | | | | | | | | | | | | | | | Merge PR #1015: Adding a function to be typically used to pass values from an... | 2017-10-03 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1080: Remove some unused parts of the reference manual. | 2017-10-03 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1076: Properly handle "coq_makefile -Q . Foo" (bug #5580). | 2017-10-03 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1072: Do not run Travis OS X packaging job on PRs | 2017-10-03 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1040: Efficient fresh name generation | 2017-10-03 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1023: dev/build/windows/makecoq_mingw.sh: install camlp5's META file | 2017-10-03 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1019: Fix BZ#5655 by avoiding the creation of a cleaner thread for ... | 2017-10-03 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1012: Make a test for coq_makefile portable. | 2017-10-03 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #667: [vernac] Remove `Qed exporting` syntax. | 2017-10-03 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | | | | | | * | | | | | | | | | Mention requiring extraction/funind in CHANGES | 2017-10-02 | |
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | |||
| | | | | | | | | | | * | | | | | | | | | | | | | | | [ide] Avoid duplicate error printing (BZ#5583) | 2017-09-29 | |
| * | | | | | | | | | | | | | | | | | | | | | | | | | [vernac] Remove `Qed exporting` syntax. | 2017-09-29 | |
|/ / / / / / / / / / / / / / / / / / / / / / / / / | |||
| | | | * | | | | | | | | | | | | | | | | | | | | | Efficient computation of the names contained in an environment. | 2017-09-28 | |
| | | | * | | | | | | | | | | | | | | | | | | | | | Efficient fresh name generation relying on sets. | 2017-09-28 | |
| |_|_|/ / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | | | | | | | | | | | * | Remove catch-all try with in the beautifier. | 2017-09-27 | |
| | | | | | | | | | | | | | | | | | | | | | | * | Beautifier gets its own formatter: fixes BZ#5704. | 2017-09-27 | |
| | | | | | | | | | | | | | | | | * | | | | | | | [stm] Warn about costly Undo operations in batch mode [BZ#5677] | 2017-09-27 | |
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | | | * | | | | | | | | [stm] Remove unused "Proof using" data in `Sync` tags. | 2017-09-27 | |
| |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | | * | | | | | | | | Browser userscript to turn BZ#XXXX occurences into links. | 2017-09-27 | |
| |_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | * | | | | | | | | Avoid looping when searching for CoqProject. | 2017-09-27 | |
| |_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | | | | | | * | | Moving setting of "cleared" evar flag directly in Evd.restrict. | 2017-09-27 | |
| | | | | | | | | | | | | | | | | | * | | Fixing an old bug in collecting evars with cleared context. | 2017-09-27 | |
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | | | | | * | | Fixing an old bug in collecting evars with cleared context. | 2017-09-27 | |
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | |||
* | | | | | | | | | | | | | | | | | | Merge PR #688: Binding universe constraints in Definition/Inductive/etc... | 2017-09-26 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | * | | | | | look for Obligation num or Next Obligation to start proof | 2017-09-26 | |
| |_|_|_|_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | |||
| | | | | | | | | | | | * | | | | | Properly display the "only" prefix for selectors (bug #5760). | 2017-09-26 | |
| |_|_|_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | |||
| | | | | | | | | | | * | | | | | Fixing a little parsing bug with level 90 introduced in 3e70ea9c. | 2017-09-25 | |
| | | | | | | | | | |/ / / / / |