| Commit message (Expand) | Author | Age | ||
|---|---|---|---|---|
| ... | ||||
| * | | | | | | | | | | | | | | | | | | 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 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | | | * | | | | | | | | | | | | | | | Mention requiring extraction/funind in CHANGES |  Tej Chajed | 2017-10-02 | |
| | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * | Remove a failwith "" |  Gaëtan Gilbert | 2017-09-29 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * | Remove unused Failure catch | Gaëtan Gilbert | 2017-09-29 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * | Remove TODO comment (Evar.t is opaque) | Gaëtan Gilbert | 2017-09-29 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * | Cleanup suggest_bullet | Gaëtan Gilbert | 2017-09-29 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * | Typo in coqdep man | Gaëtan Gilbert | 2017-09-29 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * | Remove some duplication between Typeops and Nativenorm. | Gaëtan Gilbert | 2017-09-29 | |
| | | | | | | | | | | | * | | | | | | | | | | | | | | | | | | | | | [ide] Avoid duplicate error printing (BZ#5583) |  Emilio Jesus Gallego Arias | 2017-09-29 | |
| | * | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | [vernac] Remove `Qed exporting` syntax. | Emilio Jesus Gallego Arias | 2017-09-29 | |
| |/ / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / | ||||
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * | Remove trivial TODO comment (constants can't be template poly now). | Gaëtan Gilbert | 2017-09-28 | |
| | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | * | | | | | | | | | | | | | | | | | | | | | | | | | | Efficient computation of the names contained in an environment. |  Pierre-Marie Pédrot | 2017-09-28 | |
| | | | | * | | | | | | | | | | | | | | | | | | | | | | | | | | Efficient fresh name generation relying on sets. | Pierre-Marie Pédrot | 2017-09-28 | |
| | |_|_|/ / / / / / / / / / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | | | | | | | | * | | | | | | Remove catch-all try with in the beautifier. | Théo Zimmermann | 2017-09-27 | |
| | | | | | | | | | | | | | | | | | | | | | | | * | | | | | | Beautifier gets its own formatter: fixes BZ#5704. | Théo Zimmermann | 2017-09-27 | |
| | | | | | | | | | | | | | | | | | * | | | | | | | | | | | | [stm] Warn about costly Undo operations in batch mode [BZ#5677] | Emilio Jesus Gallego Arias | 2017-09-27 | |
| | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | * | | | | | | | | | | | | | [stm] Remove unused "Proof using" data in `Sync` tags. | Emilio Jesus Gallego Arias | 2017-09-27 | |
| | |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | * | | | | | | | | | | | | | Browser userscript to turn BZ#XXXX occurences into links. | Gaëtan Gilbert | 2017-09-27 | |
| | |_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | * | | | | | | | | | | | | | Avoid looping when searching for CoqProject. | Maxime Dénès | 2017-09-27 | |
| | |_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | | | * | | | | | | | Moving setting of "cleared" evar flag directly in Evd.restrict. |  Hugo Herbelin | 2017-09-27 | |
| | | | | | | | | | | | | | | | | | | * | | | | | | | Fixing an old bug in collecting evars with cleared context. | Hugo Herbelin | 2017-09-27 | |
| | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | | * | | | | | | | Fixing an old bug in collecting evars with cleared context. | Hugo Herbelin | 2017-09-27 | |
| | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | | | | | | | | | | | Merge PR #688: Binding universe constraints in Definition/Inductive/etc... | Maxime Dénès | 2017-09-26 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | * | | | | | | | | | | look for Obligation num or Next Obligation to start proof |  Paul Steckler | 2017-09-26 | |
| | |_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | * | | | | | | | | | | Properly display the "only" prefix for selectors (bug #5760). |  Guillaume Melquiond | 2017-09-26 | |
| | |_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | | | | | * | BZ#5739, Allow level for leftmost nonterminal for printing-ony Notations | Paul Steckler | 2017-09-25 | |
| | | | | | | | | | | | * | | | | | | | | | | Fixing a little parsing bug with level 90 introduced in 3e70ea9c. | Hugo Herbelin | 2017-09-25 | |
| | | | | | | | | | | |/ / / / / / / / / / | ||||
| | | | | | | | | | | | | | | | * / / / / | [doc] Update INSTALL to match reality. | Emilio Jesus Gallego Arias | 2017-09-25 | |
| | |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | | | | | | | Merge PR #1085: Fix BZ#5755 (incorrect treatment of let-ins in parameters of ... | Maxime Dénès | 2017-09-25 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1083: Fixing bug in building _rect scheme for inductive types with ... | Maxime Dénès | 2017-09-25 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1079: Avoid generated names for html pages of the reference manual ... | Maxime Dénès | 2017-09-25 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in 4... | Maxime Dénès | 2017-09-25 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |