aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2010-08-27* (checker|kernel)/Safe_typing:regisgia
2010-08-27* (checker|kernel)/Safe_typing:regisgia
2010-08-27* toplevel/Coqtop: Reactivate -dont-load-proofs option.regisgia
2010-08-27* library/Library: Reformulate a comment.regisgia
2010-08-27* library/Library: Document.regisgia
2010-08-27* checker/SafeTyping kernel/SafeTyping:regisgia
2010-08-27* lib/Flags: Replace dont_load_proofs by load_proofs since not loadingregisgia
2010-08-27* Improve documentation of LightenLibrary.regisgia
2010-08-27* (checker|kernel)/Safe_typing: New LightenLibrary.regisgia
2010-08-27* library/Library: Remove the use of the old-fashioned lighten_library.regisgia
2010-08-27* library/Library: Remove lighten_library definition.regisgia
2010-08-26Fix an error message ot having the ERror: prefix.courtieu
2010-08-03Export printing functions for extra arguments. Maybe there's a way tomsozeau
2010-08-02Fix [clenv_missing] to compute a better approximation of missingmsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 14:17:19 +0000