aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2014-10-01Simpl less (so that cbn will not simpl too much)Pierre Boutillier
2014-10-01Fix cbn behavior wrt simpl no matchPierre Boutillier
2014-10-01Fix the refolding by cbn of mutal constants defined in not included modulesPierre Boutillier
2014-10-01Fixing nice printing of error reporting with ml tactics bound to ltac names.Hugo Herbelin
2014-10-01Made Tacsubst independent of Auto at linking time so that Tacenv doesHugo Herbelin
2014-10-01Going back on granting wish #1039 in f5d7b2b1e so that apply withHugo Herbelin
2014-10-01Fixing new failure of #3017 after 012fe1a96ba81ab (Referring to evarsHugo Herbelin
2014-10-01Fixing use of arguments renaming in apply which was broken afterHugo Herbelin
2014-10-01Updating to the new use of 3 universes, after Hurkens is simplified.Hugo Herbelin
2014-10-01STM: report the (structured) goals as XMLCarst Tankink
2014-10-01Factored out IDE goal structure.Carst Tankink
2014-10-01Add additional location information to AST XMLs.Carst Tankink
2014-10-01coq_makefile: build and install *top.cmxs pluginsEnrico Tassi
2014-10-01Removing test for bug #2080.Pierre-Marie Pédrot
2014-09-30Add a bunch of reproduction files for closed bugs.Xavier Clerc
2014-09-30Add a bunch of reproduction files for bugs.Xavier Clerc
2014-09-30Seeing IntroWildcard as an action intro pattern rather than as a naming patternHugo Herbelin
2014-09-30Add syntax for naming new goals in refine: writing ?[id] instead of _Hugo Herbelin
2014-09-30Simplify evarconv thanks to new delta status of projections,Matthieu Sozeau
2014-09-29XML pretty printing for AST (work by François Poulain, project DoCoq)Enrico Tassi
2014-09-29Notation: option to attach extra pretty printing rules to notationsEnrico Tassi
2014-09-29CoqIDE: new message to print ASTEnrico Tassi
2014-09-29typoEnrico Tassi
2014-09-29do not explode if a plugin is not up to date on -help (Close: 3673)Enrico Tassi
2014-09-29Merging some functions from evarutil.ml/evd.ml.Hugo Herbelin
2014-09-29Printing evar instance in a more intuitive order.Hugo Herbelin
2014-09-29Restoring non-uniform delta on local and global constants in 2nd orderHugo Herbelin
2014-09-29Documenting option -type-in-type.Hugo Herbelin
2014-09-29Adding a test for bug #2428.Pierre-Marie Pédrot
2014-09-29Bug fixed.Matthieu Sozeau
2014-09-29Fix test-suite filesMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 16:55:32 +0000