aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* Make tclEFFECTS also update the env in the proof monadGravatar Enrico Tassi2014-10-06
* fix wrong escaping in coq_makefileGravatar Enrico Tassi2014-10-06
* decl_mode: stay in declarative modeGravatar Enrico Tassi2014-10-06
* Semantic fix of a refine in Rewrite.Gravatar Pierre-Marie Pédrot2014-10-05
* Check compatibility of types in change depending on whether it is aGravatar Hugo Herbelin2014-10-05
* A few improvements on pattern-matching compilation.Gravatar Hugo Herbelin2014-10-05
* A few Global.env removed.Gravatar Hugo Herbelin2014-10-04
* Fixing #3193 (honoring implicit arguments in local definitions).Gravatar Hugo Herbelin2014-10-03
* Classify segfaults as failures in opened bugs.Gravatar Xavier Clerc2014-10-03
* Classify segfaults as failures in opened bugsGravatar Xavier Clerc2014-10-03
* Fixing #3606 continued (doc of Scheme Boolean Equality Scheme).Gravatar Hugo Herbelin2014-10-03
* Removing deactivated command Show Tree.Gravatar Hugo Herbelin2014-10-03
* Fixing #3657 (check that both sides of a "change with" have the sameGravatar Hugo Herbelin2014-10-03
* Test for bug #3652 fixed in 0fb36157b9baGravatar Hugo Herbelin2014-10-03
* Fixing ennoying warning about evars named ?23 and so on.Gravatar Hugo Herbelin2014-10-03
* Fixing #3623 (unbound evars in types in a call to "change with").Gravatar Hugo Herbelin2014-10-03
* Add a bunch of reproduction files for bugs.Gravatar Xavier Clerc2014-10-03
* Fixing #3634 (wrong env in "cannot instantiate because not in itsGravatar Hugo Herbelin2014-10-03
* Adapting output/Arguments_renaming continued.Gravatar Hugo Herbelin2014-10-03
* Implement module subtyping for polymorphic constants (errors onGravatar Matthieu Sozeau2014-10-02
* Fixing interpretation of constr under binders which was broken afterGravatar Hugo Herbelin2014-10-02
* Fixing bug #2810 (autounfold on local variable declared as hint but cleared).Gravatar Hugo Herbelin2014-10-02
* Completing fixing order of parameters when translating fromGravatar Hugo Herbelin2014-10-02
* An evar name changed in output test.Gravatar Hugo Herbelin2014-10-02
* Adapting the output test Notations:Gravatar Hugo Herbelin2014-10-02
* Added make dependency in %.out in output tests.Gravatar Hugo Herbelin2014-10-02
* Revert "test-suite: New names for vars but the expected invariant is preserved"Gravatar Hugo Herbelin2014-10-02
* Adapting output/Arguments_renaming.out after fixing printing ofGravatar Hugo Herbelin2014-10-02
* Print type and environment of unsolved holes.Gravatar Arnaud Spiwack2014-10-02
* Work around issues with FO unification trying to unify terms ofGravatar Matthieu Sozeau2014-10-02
* Move eta-expansion after delta reduction in kernel reduction. This makesGravatar Matthieu Sozeau2014-10-02
* Fix treatment of projections in Cst_stacks and unfolding behavior in evarconv.Gravatar Matthieu Sozeau2014-10-02
* eta contractionsGravatar Pierre Boutillier2014-10-01
* argument flip of Cyclic31.nshiftr and Cyclic31.nshiftlGravatar Pierre Boutillier2014-10-01
* Simpl less (so that cbn will not simpl too much)Gravatar Pierre Boutillier2014-10-01
* Fix cbn behavior wrt simpl no matchGravatar Pierre Boutillier2014-10-01
* Fix the refolding by cbn of mutal constants defined in not included modulesGravatar Pierre Boutillier2014-10-01
* Fixing nice printing of error reporting with ml tactics bound to ltac names.Gravatar Hugo Herbelin2014-10-01
* Made Tacsubst independent of Auto at linking time so that Tacenv doesGravatar Hugo Herbelin2014-10-01
* Going back on granting wish #1039 in f5d7b2b1e so that apply withGravatar Hugo Herbelin2014-10-01
* Fixing new failure of #3017 after 012fe1a96ba81ab (Referring to evarsGravatar Hugo Herbelin2014-10-01
* Fixing use of arguments renaming in apply which was broken afterGravatar Hugo Herbelin2014-10-01
* Updating to the new use of 3 universes, after Hurkens is simplified.Gravatar Hugo Herbelin2014-10-01
* STM: report the (structured) goals as XMLGravatar Carst Tankink2014-10-01
* Factored out IDE goal structure.Gravatar Carst Tankink2014-10-01
* Add additional location information to AST XMLs.Gravatar Carst Tankink2014-10-01
* coq_makefile: build and install *top.cmxs pluginsGravatar Enrico Tassi2014-10-01
* Removing test for bug #2080.Gravatar Pierre-Marie Pédrot2014-10-01
* Add a bunch of reproduction files for closed bugs.Gravatar Xavier Clerc2014-09-30
* Add a bunch of reproduction files for bugs.Gravatar Xavier Clerc2014-09-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 01:55:10 +0000