aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2014-10-03Fixing ennoying warning about evars named ?23 and so on.Hugo Herbelin
2014-10-03Fixing #3623 (unbound evars in types in a call to "change with").Hugo Herbelin
2014-10-03Add a bunch of reproduction files for bugs.Xavier Clerc
2014-10-03Fixing #3634 (wrong env in "cannot instantiate because not in itsHugo Herbelin
2014-10-03Adapting output/Arguments_renaming continued.Hugo Herbelin
2014-10-02Implement module subtyping for polymorphic constants (errors onMatthieu Sozeau
2014-10-02Fixing interpretation of constr under binders which was broken afterHugo Herbelin
2014-10-02Fixing bug #2810 (autounfold on local variable declared as hint but cleared).Hugo Herbelin
2014-10-02Completing fixing order of parameters when translating fromHugo Herbelin
2014-10-02An evar name changed in output test.Hugo Herbelin
2014-10-02Adapting the output test Notations:Hugo Herbelin
2014-10-02Added make dependency in %.out in output tests.Hugo Herbelin
2014-10-02Revert "test-suite: New names for vars but the expected invariant is preserved"Hugo Herbelin
2014-10-02Adapting output/Arguments_renaming.out after fixing printing ofHugo Herbelin
2014-10-02Print type and environment of unsolved holes.Arnaud Spiwack
2014-10-02Work around issues with FO unification trying to unify terms ofMatthieu Sozeau
2014-10-02Move eta-expansion after delta reduction in kernel reduction. This makesMatthieu Sozeau
2014-10-02Fix treatment of projections in Cst_stacks and unfolding behavior in evarconv.Matthieu Sozeau
2014-10-01eta contractionsPierre Boutillier
2014-10-01argument flip of Cyclic31.nshiftr and Cyclic31.nshiftlPierre Boutillier
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 21:04:10 +0000