aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Implementing a generic mechanism for locating named objects from Coq side.Gravatar Pierre-Marie Pédrot2017-10-03
* Moving the Ltac-specific part of the nametab to the Ltac plugin.Gravatar Pierre-Marie Pédrot2017-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
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ 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
| |_|_|/ / / / / / / / / / / / / |/| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | * [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
| |_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | |
* | | | | | | | | | | | | Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Gravatar Maxime Dénès2017-09-26
|\ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | * look for Obligation num or Next Obligation to start proofGravatar Paul Steckler2017-09-26
| |_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | |
| | | | | | | | | | | | * Properly display the "only" prefix for selectors (bug #5760).Gravatar Guillaume Melquiond2017-09-26
| |_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | |
| | | | | | | | | | | * Fixing a little parsing bug with level 90 introduced in 3e70ea9c.Gravatar Hugo Herbelin2017-09-25
| | | | | | | | | | |/
* | | | | | | | | | | Merge PR #1085: Fix BZ#5755 (incorrect treatment of let-ins in parameters of ...Gravatar Maxime Dénès2017-09-25
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #1083: Fixing bug in building _rect scheme for inductive types with ...Gravatar Maxime Dénès2017-09-25
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1079: Avoid generated names for html pages of the reference manual ...Gravatar Maxime Dénès2017-09-25
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in 4...Gravatar Maxime Dénès2017-09-25
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1057: Reporting locations in error messages about notation formats.Gravatar Maxime Dénès2017-09-25
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1060: An optimization of tactic constructorGravatar Maxime Dénès2017-09-25
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1075: Re-enable checker error messagesGravatar Maxime Dénès2017-09-25
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | |
| | | | | | | * | | | | | | | | | Discharge.ml: cosmetic renaming of some variables.Gravatar Hugo Herbelin2017-09-23
| | | | | | | * | | | | | | | | | Fixing #5755 (discharging of inductive types not correct with let-ins).Gravatar Hugo Herbelin2017-09-23
| |_|_|_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | * After testing it in live, writing metas using an ?INTERNAL#42 style is ugly.Gravatar Hugo Herbelin2017-09-23
| |_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | |
| | | | * | | | | | | | | | | Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791).Gravatar Hugo Herbelin2017-09-23
| | | | | | * | | | | | | | | Fixing _rect bug for inductive types with let-ins and non-rec uniform params.Gravatar Hugo Herbelin2017-09-23
| |_|_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | |
| | | | | | | | | | | | * | Remove some unused parts of the reference manual.Gravatar Guillaume Melquiond2017-09-22
| |_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | |
| | | | | * | | | | | | | Avoid generated names for html pages of the reference manual (bug #4742).Gravatar Guillaume Melquiond2017-09-22
| |_|_|_|/ / / / / / / / |/| | | | | | | | | | |
| | | | | | * | | | | | Make a test for coq_makefile portable.Gravatar Pierre-Marie Pédrot2017-09-22
* | | | | | | | | | | | Merge PR #1055: Remove STM vernacularsGravatar Maxime Dénès2017-09-22
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1065: In gitlab set TRAVIS_BRANCH so user overlays will work as exp...Gravatar Maxime Dénès2017-09-22
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1074: Fix BZ#5750 (recovering ability to print the hole of a contex...Gravatar Maxime Dénès2017-09-22
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-01 11:35:05 +0000