| Commit message (Expand) | Author | Age | ||
|---|---|---|---|---|
| ... | ||||
| * | | | | | | | | | | | | | | | | | | Fix typo in INSTALL |  Maxime Dénès | 2017-10-05 | |
| * | | | | | | | | | | | | | | | | | | Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 t... | Maxime Dénès | 2017-10-05 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1093: [doc] Update INSTALL to match reality. | Maxime Dénès | 2017-10-05 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1107: Add coqwc tests to test suite | Maxime Dénès | 2017-10-05 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | * | | | | | | | | | | | | | | GitLab CI: make all_stdlib.v in build job |  Gaëtan Gilbert | 2017-10-05 | |
| * | | | | | | | | | | | | | | | | | | | | | Merge PR #1106: Fix beautifier | Maxime Dénès | 2017-10-05 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1102: On the detection of evars which "advanced" (and a fix to BZ#5... | Maxime Dénès | 2017-10-05 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1101: Fixing an old proof engine bug in collecting evars with clear... | Maxime Dénès | 2017-10-05 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1059: coq_makefile: make sure compile flags for Coq and coq_makefil... | Maxime Dénès | 2017-10-05 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #1112: Fix GeoCoq CI and remove it from allowed failures | Maxime Dénès | 2017-10-05 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | | * | | | | | | | | | | | | | Extraction: reduce eta-redexes whose cores are atomic (solves indirectly BZ#4... |  Pierre Letouzey | 2017-10-05 | |
| | |_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | * | | | | | | | | Shorten the .gitattributes file. |  Théo Zimmermann | 2017-10-05 | |
| | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | * | | | | | | | | | | | [pp] Minor optimization in `Pp.t` construction and gluing. |  Emilio Jesus Gallego Arias | 2017-10-05 | |
| | |_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | * | | | | | | | | | | | [ci] Remove deploy to GitHub of OS X package. | Théo Zimmermann | 2017-10-05 | |
| | | | | | | | | | | | | | * | | | | | | | | | Fixing BZ#5769 (variable of type "_something" was named after invalid "_"). |  Hugo Herbelin | 2017-10-05 | |
| | | | | | | | | | | | | | * | | | | | | | | | Distinguishing pseudo-letters out of the set of unicode letters. | Hugo Herbelin | 2017-10-05 | |
| | | | | | | | | | | | | | * | | | | | | | | | Fixing typos in comments of unicode.ml. | Hugo Herbelin | 2017-10-05 | |
| | | | | | | | | | | | | | | |_|_|_|_|_|_|/ | | | | | | | | | | | | | |/| | | | | | | | ||||
| | | | | | | | | | | | | * / | | | | | | | | Fixing #5765 (an anomaly with 'pat in parameters of inductive definition). | Hugo Herbelin | 2017-10-05 | |
| | | | | | | | | | | | | |/ / / / / / / / | ||||
| * | | | | | | | | | | | | | | | | | | | | Merge PR #1006: fix: ssrmatching and primitive projections | Maxime Dénès | 2017-10-04 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1078: Report missing arguments in error message | Maxime Dénès | 2017-10-04 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | | | | | * | | | | | | | Extraction : minor support stuff for the new Extraction Compute plugin | Pierre Letouzey | 2017-10-04 | |
| | | | | | | | | | | | | | | |/ / / / / / / | | | | | | | | | | | | | |/| | | | | | | | ||||
| * | | | | | | | | | | | | | | | | | | | | | Merge PR #1096: [stm] Warn about costly Undo operations in batch mode [BZ#5677] | Maxime Dénès | 2017-10-04 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | | | | | | * | | | | | | [ci] Remove temporary bignums overlay. | Théo Zimmermann | 2017-10-04 | |
| | | | | | | | | | | | | | | | |/ / / / / / | | | | | | | | | | | | | | |/| | | | | | | ||||
| * | | | | | | | | | | | | | | | | | | | | | Merge PR #1058: Fixing BZ#5741 (anomaly in info_trivial). | Maxime Dénès | 2017-10-04 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | * | | | | | | | | | | | add coqwc tests |  Paul Steckler | 2017-10-03 | |
| | | | | | | | | | | | |_|_|_|/ / / / / / | | | | | | | | | | |/| | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | | | * | | autolink to Github PRs from Bugzilla | Paul Steckler | 2017-10-03 | |
| | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | | * | | Ltac uses the new generic locatable API. |  Pierre-Marie Pédrot | 2017-10-03 | |
| | | | | | | | | | | | | | | | | | * | | Implementing a generic mechanism for locating named objects from Coq side. | Pierre-Marie Pédrot | 2017-10-03 | |
| | | | | | | | | | | | | | | | | | * | | Moving the Ltac-specific part of the nametab to the Ltac plugin. | Pierre-Marie Pédrot | 2017-10-03 | |
| | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | ||||
| | | | | | | * | | | | | | | | | | | | fix compilation on OCaml < 4.04 |  Enrico Tassi | 2017-10-03 | |
| * | | | | | | | | | | | | | | | | | | Merge PR #1110: Mention requiring extraction/funind in CHANGES | Maxime Dénès | 2017-10-03 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1105: [stm] Remove unused "Proof using" data in `Sync` tags. | Maxime Dénès | 2017-10-03 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1104: Browser userscript to turn BZ#XXXX occurences into links. | Maxime Dénès | 2017-10-03 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1100: Avoid looping when searching for CoqProject. | Maxime Dénès | 2017-10-03 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1099: BZ#5637, look for Obligation num or Next Obligation to start ... | Maxime Dénès | 2017-10-03 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1097: Properly display the "only" prefix for selectors (bug #5760). | Maxime Dénès | 2017-10-03 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1094: Fixing a little parsing bug with level 90 introduced in 3e70e... | Maxime Dénès | 2017-10-03 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1090: [ide] Avoid duplicate error printing (BZ#5583) | Maxime Dénès | 2017-10-03 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1084: After testing it in live, writing metas using an ?INTERNAL#42... | Maxime Dénès | 2017-10-03 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | | | | * | | | | | | | | | | | | | Remove GeoCoq from allowed failures. | Théo Zimmermann | 2017-10-03 | |
| | | | | | | | | | | | | | | * | | | | | | | | | | | | | Fix GeoCoq build by using a shared CI configure. | Théo Zimmermann | 2017-10-03 | |
| | |_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #1015: Adding a function to be typically used to pass values from an... | Maxime Dénès | 2017-10-03 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1080: Remove some unused parts of the reference manual. | Maxime Dénès | 2017-10-03 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1076: Properly handle "coq_makefile -Q . Foo" (bug #5580). | Maxime Dénès | 2017-10-03 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1072: Do not run Travis OS X packaging job on PRs | Maxime Dénès | 2017-10-03 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1040: Efficient fresh name generation | Maxime Dénès | 2017-10-03 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1023: dev/build/windows/makecoq_mingw.sh: install camlp5's META file | Maxime Dénès | 2017-10-03 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1019: Fix BZ#5655 by avoiding the creation of a cleaner thread for ... | Maxime Dénès | 2017-10-03 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1012: Make a test for coq_makefile portable. | Maxime Dénès | 2017-10-03 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #667: [vernac] Remove `Qed exporting` syntax. | Maxime Dénès | 2017-10-03 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |