aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-10-03Merge PR #1097: Properly display the "only" prefix for selectors (bug #5760).Maxime Dénès
2017-10-03Merge PR #1094: Fixing a little parsing bug with level 90 introduced in 3e70e...Maxime Dénès
2017-10-03Merge PR #1090: [ide] Avoid duplicate error printing (BZ#5583)Maxime Dénès
2017-10-03Merge PR #1084: After testing it in live, writing metas using an ?INTERNAL#42...Maxime Dénès
2017-10-03Merge PR #1015: Adding a function to be typically used to pass values from an...Maxime Dénès
2017-10-03Merge PR #1080: Remove some unused parts of the reference manual.Maxime Dénès
2017-10-03Merge PR #1076: Properly handle "coq_makefile -Q . Foo" (bug #5580).Maxime Dénès
2017-10-03Merge PR #1072: Do not run Travis OS X packaging job on PRsMaxime Dénès
2017-10-03Merge PR #1040: Efficient fresh name generationMaxime Dénès
2017-10-03Merge PR #1023: dev/build/windows/makecoq_mingw.sh: install camlp5's META fileMaxime Dénès
2017-10-03Merge PR #1019: Fix BZ#5655 by avoiding the creation of a cleaner thread for ...Maxime Dénès
2017-10-03Merge PR #1012: Make a test for coq_makefile portable.Maxime Dénès
2017-10-03Merge PR #667: [vernac] Remove `Qed exporting` syntax.Maxime Dénès
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-28Efficient computation of the names contained in an environment.Pierre-Marie Pédrot
2017-09-28Efficient fresh name generation relying on sets.Pierre-Marie Pédrot
2017-09-26Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Maxime Dénès
2017-09-26Properly display the "only" prefix for selectors (bug #5760).Guillaume Melquiond
2017-09-25Fixing a little parsing bug with level 90 introduced in 3e70ea9c.Hugo Herbelin
2017-09-25Merge PR #1085: Fix BZ#5755 (incorrect treatment of let-ins in parameters of ...Maxime Dénès
2017-09-25Merge PR #1083: Fixing bug in building _rect scheme for inductive types with ...Maxime Dénès
2017-09-25Merge PR #1079: Avoid generated names for html pages of the reference manual ...Maxime Dénès
2017-09-25Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in 4...Maxime Dénès
2017-09-25Merge PR #1057: Reporting locations in error messages about notation formats.Maxime Dénès
2017-09-25Merge PR #1060: An optimization of tactic constructorMaxime Dénès
2017-09-25Merge PR #1075: Re-enable checker error messagesMaxime Dénès
2017-09-23Discharge.ml: cosmetic renaming of some variables.Hugo Herbelin
2017-09-23Fixing #5755 (discharging of inductive types not correct with let-ins).Hugo Herbelin
2017-09-23After testing it in live, writing metas using an ?INTERNAL#42 style is ugly.Hugo Herbelin
2017-09-23Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791).Hugo Herbelin
2017-09-23Fixing _rect bug for inductive types with let-ins and non-rec uniform params.Hugo Herbelin
2017-09-22Remove some unused parts of the reference manual.Guillaume Melquiond
2017-09-22Avoid generated names for html pages of the reference manual (bug #4742).Guillaume Melquiond
2017-09-22Make a test for coq_makefile portable.Pierre-Marie Pédrot
2017-09-22Merge PR #1055: Remove STM vernacularsMaxime Dénès
2017-09-22Merge PR #1065: In gitlab set TRAVIS_BRANCH so user overlays will work as exp...Maxime Dénès
2017-09-22Merge PR #1074: Fix BZ#5750 (recovering ability to print the hole of a contex...Maxime Dénès
2017-09-22Merge PR #1071: Mark "Set Tactic Compat Context" as deprecated.Maxime Dénès
2017-09-22Merge PR #1070: Remove remaining occurrences of -just-parsing.Maxime Dénès
2017-09-22Merge PR #1064: coq_makefile: dont show errors from failed (ignored) rmdirMaxime Dénès
2017-09-22Merge PR #1063: [flags] Flag `open Flags`Maxime Dénès
2017-09-22Merge PR #1061: Fix appveyor buildMaxime Dénès
2017-09-21Properly handle "coq_makefile -Q . Foo" (bug #5580).Guillaume Melquiond
2017-09-21Fix -silent flag of coqchk after ff918e4.Maxime Dénès
2017-09-21Adapt checker to change in locations.Maxime Dénès
2017-09-21Proposing meta names more distinguishable from evar names than ?M42.Hugo Herbelin
2017-09-21A possible fix to BZ#5750 (ability to print context of ltac subterm match).Hugo Herbelin
2017-09-21[checker] Add missing Feedback printer (BZ#5587)Emilio Jesus Gallego Arias
2017-09-21Do not run Travis OS X packaging job on PRsThéo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-09 04:22:24 +0000