aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-05-28Test for 4159Enrico Tassi
2015-05-27Fix bug #4159Matthieu Sozeau
2015-05-26Jump to error line in CoqIDE grabs focus of the textview.Pierre-Marie Pédrot
2015-05-25CoqIDE columns in error and job panels can be sorted.Pierre-Marie Pédrot
2015-05-22Continuing 4b5af0d6e9 and 69941d4e19 about filename case check on MacOS X.Hugo Herbelin
2015-05-21Changing the heuristic fixing bug #4241.Pierre Courtieu
2015-05-20Answering report #4241 (formatting of boxes not behaving regularlyHugo Herbelin
2015-05-20Continuing incomplete 4b5af0d6e9ec1 (on MacOS X, ensuring that filesHugo Herbelin
2015-05-19Adding an extensible global state to evarmaps.Pierre-Marie Pédrot
2015-05-19Test for bug #4116.Pierre-Marie Pédrot
2015-05-18Uncaught exception termination exits coqtop with the anomaly errno.Pierre-Marie Pédrot
2015-05-18The Fail command does not catch uncaught exception anomalies anymore.Pierre-Marie Pédrot
2015-05-18Removing test for opened bugs that were already present in the closed test-su...Pierre-Marie Pédrot
2015-05-18Tentative fix for #3461: Anomaly: Uncaught exception Pretype_errors.PretypeEr...Pierre-Marie Pédrot
2015-05-18Fixed CHANGES to reflect -color option.Pierre Courtieu
2015-05-18Disabling colors when tERM variable is "dumb".Pierre Courtieu
2015-05-18Fix usage about -color.Pierre Courtieu
2015-05-18Adding the -color option to coqc.Pierre Courtieu
2015-05-17Fixing bug #4201: The native compiler is not race-free.Pierre-Marie Pédrot
2015-05-16Fixing bug #2814: "Anomaly: Uncaught exception Option.IsNone".Pierre-Marie Pédrot
2015-05-15Removing option -no-native-compiler from test #3539 since this option is nowHugo Herbelin
2015-05-15On MacOS X, ensuring that files found in the file system have theHugo Herbelin
2015-05-15Granting wish #4048: Locate Ltac prints the source of redefined Ltac.Pierre-Marie Pédrot
2015-05-15Make Coercion.inh_app_fun respect its specification.Pierre-Marie Pédrot
2015-05-14Do not regenerate .d files when cleaning them. (Fix bug #4079)Guillaume Melquiond
2015-05-14The -list-tag options now prints the corresponding COQ_COLORS value.Pierre-Marie Pédrot
2015-05-14Adding an option -w to control Coq warning output.Pierre-Marie Pédrot
2015-05-14Disable precompilation for native_compute by default.Guillaume Melquiond
2015-05-13Fixing bug #4216:Pierre-Marie Pédrot
2015-05-13Safer typing primitives.Pierre-Marie Pédrot
2015-05-13Better error message for non-existent required libraries with a From prefix.Pierre-Marie Pédrot
2015-05-13Fix for a second avatar of bug #4234.Pierre-Marie Pédrot
2015-05-13Documenting Set Regular Subst Tactic (though unsure this is worth theHugo Herbelin
2015-05-13Better fixing #4198 such that the term to match is looked for beforeHugo Herbelin
2015-05-13Documenting the Loose Hint Behavior flag.Pierre-Marie Pédrot
2015-05-12List.nth_error directly produces Some/None instead of value/errorPierre Letouzey
2015-05-12Mark PreOrder as a consequence of Equivalence. (Fix bug #4213)Guillaume Melquiond
2015-05-12Fix my previous commit on ~polypropPierre Letouzey
2015-05-12Adding an option Loose Hint Behavior to handle hints loaded but not imported.Pierre-Marie Pédrot
2015-05-12Adding unique identifiers to hints.Pierre-Marie Pédrot
2015-05-12Extraction: fix the detection of the "polyprop" situationPierre Letouzey
2015-05-12Test for bug #4234.Pierre-Marie Pédrot
2015-05-12Fixing bug #4234.Pierre-Marie Pédrot
2015-05-12nice error for Restart outside a proof (Close: #4235)Enrico Tassi
2015-05-12STM: process_error_hook set in Vernac where fname is known (fix #4229)Enrico Tassi
2015-05-11Adding a test to check whether two tactic notations conflict.Pierre-Marie Pédrot
2015-05-11Test for bug #4232.Pierre-Marie Pédrot
2015-05-11Fixing bug #4232.Pierre-Marie Pédrot
2015-05-11Rationalizing a bit the interface of Hints.Pierre-Marie Pédrot
2015-05-10Code factorization in Constr_matching.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 07:09:26 +0000