aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-10-13STM: simplify how the term part of a side effect is retrievedEnrico Tassi
2014-10-13library/opaqueTables: enable their use in interactive modeEnrico Tassi
2014-10-13Coqinit: look in toploop/ even if configured with -localEnrico Tassi
2014-10-13Mentioning incompatibility shown in #3718 and coming from #3050Hugo Herbelin
2014-10-12Tentative fix for a badly used Option.get in Reductionops.Pierre-Marie Pédrot
2014-10-11Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameMatthieu Sozeau
2014-10-10Do not expand primitive projections eagerly in evarconv, but onlyMatthieu Sozeau
2014-10-10Give the same argument name for the record binder of type classMatthieu Sozeau
2014-10-10Add debug printers for projections, fix printing of evar constraintsMatthieu Sozeau
2014-10-10Add a "Debug Tactic Unification" option and correct the first-orderMatthieu Sozeau
2014-10-10Make constrMatching and detyping more robust with respect toMatthieu Sozeau
2014-10-10Fix bug due to shadowing a variable name in tacredMatthieu Sozeau
2014-10-10Fix segfault in native compiler on int31 division.Maxime Dénès
2014-10-09No need anymore for referring to xml directory in MLINCLUDES.Hugo Herbelin
2014-10-09Restoring plugins/xml/README erased by mistake.Hugo Herbelin
2014-10-09Propagating name of goal to main subgoal in cut and conversion tactics.Hugo Herbelin
2014-10-09Added support for having one subgoal inheriting the name of its father in Ref...Hugo Herbelin
2014-10-09Removing Convert_concl and Convert_hyp from Logic.Hugo Herbelin
2014-10-09A version of convert_concl and convert_hyp in new proof engine.Hugo Herbelin
2014-10-09Adding printer for named_context_val and Goal.goal in debugger.Hugo Herbelin
2014-10-09Fixup leading ./ path cleaningPierre Boutillier
2014-10-09Coq_makefile: Allow empty logical namesPierre Boutillier
2014-10-08fix make mlidocPierre Boutillier
2014-10-08Fixing the anomaly in bug #3045 (a filter was not type-safe inHugo Herbelin
2014-10-08Applying Virgile Prevosto's patch for better error report in coqdep (#3029).Hugo Herbelin
2014-10-08Forgotten hints.ml{,i} files in 38b34dfffcc.Hugo Herbelin
2014-10-07Adding a printer for hints.Hugo Herbelin
2014-10-07Splitting out of auto.ml a file hints.ml dedicated to hints so as toHugo Herbelin
2014-10-07Add test-suite file for the projection unfolding bug I just fixed.Matthieu Sozeau
2014-10-07Fix test-suite file 3352 which was containing the wrong test.Matthieu Sozeau
2014-10-07Fix test-suite file to test original bug, not the failure of the guardMatthieu Sozeau
2014-10-07Build unfolded versions of the primitive projection in let (a, p) := ...Matthieu Sozeau
2014-10-07Fixing #3687 (inconsistent lexer state after a bullet).Hugo Herbelin
2014-10-07Removing debugging information committed by mistake.Hugo Herbelin
2014-10-07Avoid a warning with Meta's names in debugger.Hugo Herbelin
2014-10-07coq_makefile: explicit target install-toploop for toploop pluginsEnrico Tassi
2014-10-06Make tclEFFECTS also update the env in the proof monadEnrico Tassi
2014-10-06fix wrong escaping in coq_makefileEnrico Tassi
2014-10-06decl_mode: stay in declarative modeEnrico Tassi
2014-10-05Semantic fix of a refine in Rewrite.Pierre-Marie Pédrot
2014-10-05Check compatibility of types in change depending on whether it is aHugo Herbelin
2014-10-05A few improvements on pattern-matching compilation.Hugo Herbelin
2014-10-04A few Global.env removed.Hugo Herbelin
2014-10-03Fixing #3193 (honoring implicit arguments in local definitions).Hugo Herbelin
2014-10-03Classify segfaults as failures in opened bugs.Xavier Clerc
2014-10-03Classify segfaults as failures in opened bugsXavier Clerc
2014-10-03Fixing #3606 continued (doc of Scheme Boolean Equality Scheme).Hugo Herbelin
2014-10-03Removing deactivated command Show Tree.Hugo Herbelin
2014-10-03Fixing #3657 (check that both sides of a "change with" have the sameHugo Herbelin
2014-10-03Test for bug #3652 fixed in 0fb36157b9baHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 12:41:28 +0000