aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2010-09-27Fix bug in implementation of setoid rewriting under cases andmsozeau
2010-09-24Fixed a bug in printing fix/cofix error messages when severalherbelin
2010-09-24Solving bug #2212 (unification under tuples now not allowed forherbelin
2010-09-24Partial review of removed dead code (r13460)herbelin
2010-09-24Checker: remove some dead codeletouzey
2010-09-24Dead code in extractionletouzey
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-09-24dev/Makefile.oug: how to run the Oug analyser, for instance for finding dead ...letouzey
2010-09-23Added a section in the documentation of Vernacular commands about Set/Unset/T...aspiwack
2010-09-23Update CHANGES: Local/Global Set/Unset.aspiwack
2010-09-23Fix inconsistency in Prop/Set conversion checkglondu
2010-09-21Report fix bug 2345 from v8.3 (Bad error message when functionalcourtieu
2010-09-20Added eta-expansion in kernel, type inference and tactic unification,herbelin
2010-09-20Fixed test of bug #2360 (use of Fail to check a regular error insteadherbelin
2010-09-20Extraction: re-introduce some eta-expansions in rare situations leading to '_...letouzey
2010-09-19Fixing bug #2389 (keyword "Declare Instance" unknown from "coqdoc -g") butherbelin
2010-09-19Fixing bug #2360 (descend_in_conjunctions built ill-typed terms). Shouldn't weherbelin
2010-09-19Reverting partial fix for #2335 committed by mistake in r13435. Sorry.herbelin
2010-09-19Hopefully a fix for #2176 (redirection not understood with some shells)herbelin
2010-09-19Addressing part 2 of bug report 2377 (removing intrusive warning whenherbelin
2010-09-19Patch solving the bug but leaving open design choicesherbelin
2010-09-18Fixing #2162 and #2367 (wrong order of Show Match) for branch 8.2 tooherbelin
2010-09-18Added test for bugs 2242, 2337, 2339 + remove the use of name "ambiguous" inherbelin
2010-09-18Fixing bugs #2347 (part 2) and #2388: error message printing was doneherbelin
2010-09-18Now prints an error instead of an anomaly when dynlink failsherbelin
2010-09-17Fixed a problem introduced in r12607 after pattern_of_constr servedherbelin
2010-09-17In the computation of missing arguments for apply, accept that theherbelin
2010-09-17For the moment, two small manual eta-expansions to avoid '_a after extractionletouzey
2010-09-17Extraction: multiple fixes related with the Not_found encountered by X. Leroyletouzey
2010-09-17Coqdep_boot : misc improvementsletouzey
2010-09-16Explicit Mod_checking signatureglondu
2010-09-15Sharing is not anymore broken by traverse_module.soubiran
2010-09-15Fix likely semantic typosglondu
2010-09-14CoqIDE argv parsing delegated to coqtopvgross
2010-09-13Fix unescaped end-of-lines (OCaml warning 29)glondu
2010-09-13commit 13400 and 13409.soubiran
2010-09-11Improving a few error messages in Ltac interpretationherbelin
2010-09-10files introduce in commit 13401 aren't erased anymore by 'make clean'pboutill
2010-09-10Bugfix: A notation for a constructor where some arguments are _pboutill
2010-09-09NMake : another round of heavy reworkletouzey
2010-09-06Added doc/refman/coqide.eps and coqide-queries.eps to remove the need for png...emakarov
2010-09-02fixed bug #2375 (congruence)corbinea
2010-09-02* removed declare_constant and declare_internal_constant vsiles
2010-09-02v13392 port from v8.3 to trunk : correct message when defining inductive schemesvsiles
2010-09-02Clarified role of Set Boolean Equality Schemes wrt Set Equality Scheme +herbelin
2010-09-02Improved printing of Unfoldable constants in hints databases (usedherbelin
2010-08-31* By default, load proof terms.regisgia
2010-08-27* scripts/Coqc toplevel/Usage:regisgia
2010-08-27* checker/Safe_typing.LightenLibrary:regisgia
2010-08-27* kernel/Safe_typing.LightenLibrary:regisgia
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 02:58:00 +0000