aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2015-05-09Adjusting test-suite after 5cbc018fe9347 (subst as in 8.4 by default).Hugo Herbelin
2015-05-09Adding a flag "Set Regular Subst Tactic" off by default in v8.5 forHugo Herbelin
2015-05-08A more user-friendly naming of variables of ltac names defined byHugo Herbelin
2015-05-06Fixing treatment of recursive equations damaged by 857e82b2ca0d1.Hugo Herbelin
2015-05-06Fixing "subst" to respect v8.4 most-ancient to most-recent hyps orderHugo Herbelin
2015-05-05Compatibility ocaml 3.12.Hugo Herbelin
2015-05-05Granting wish #4221.Pierre-Marie Pédrot
2015-05-05Fix bug #4212, congruence forgetting about some universe constraints.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 16:56:29 +0000