Commit message (Expand) | Author | Age | |
---|---|---|---|
* | 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 | |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | 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 | |
| |_|_|/ / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | | | * | [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 | |
| |_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | |||
* | | | | | | | | | | | | | 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 | |
| | | | | | | | | | |/ | |||
* | | | | | | | | | | | Merge PR #1085: Fix BZ#5755 (incorrect treatment of let-ins in parameters of ... | 2017-09-25 | |
|\ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1083: Fixing bug in building _rect scheme for inductive types with ... | 2017-09-25 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1079: Avoid generated names for html pages of the reference manual ... | 2017-09-25 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in 4... | 2017-09-25 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1057: Reporting locations in error messages about notation formats. | 2017-09-25 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1060: An optimization of tactic constructor | 2017-09-25 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1075: Re-enable checker error messages | 2017-09-25 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | |||
| | | | | | | * | | | | | | | | | | Discharge.ml: cosmetic renaming of some variables. | 2017-09-23 | |
| | | | | | | * | | | | | | | | | | Fixing #5755 (discharging of inductive types not correct with let-ins). | 2017-09-23 | |
| |_|_|_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | | | * | After testing it in live, writing metas using an ?INTERNAL#42 style is ugly. | 2017-09-23 | |
| |_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | |||
| | | | * | | | | | | | | | | | Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791). | 2017-09-23 | |
| | | | | | * | | | | | | | | | Fixing _rect bug for inductive types with let-ins and non-rec uniform params. | 2017-09-23 | |
| |_|_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | | |||
| | | | | | | | | | | | * | | Remove some unused parts of the reference manual. | 2017-09-22 | |
| |_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | |||
| | | | | * | | | | | | | | Avoid generated names for html pages of the reference manual (bug #4742). | 2017-09-22 | |
| |_|_|_|/ / / / / / / / |/| | | | | | | | | | | | |||
| | | | | | * | | | | | | Make a test for coq_makefile portable. | 2017-09-22 | |
* | | | | | | | | | | | | Merge PR #1055: Remove STM vernaculars | 2017-09-22 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1065: In gitlab set TRAVIS_BRANCH so user overlays will work as exp... | 2017-09-22 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1074: Fix BZ#5750 (recovering ability to print the hole of a contex... | 2017-09-22 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1071: Mark "Set Tactic Compat Context" as deprecated. | 2017-09-22 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #1070: Remove remaining occurrences of -just-parsing. | 2017-09-22 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |