aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* 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
* Seeing IntroWildcard as an action intro pattern rather than as a naming patternGravatar Hugo Herbelin2014-09-30
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* Simplify evarconv thanks to new delta status of projections,Gravatar Matthieu Sozeau2014-09-30
* XML pretty printing for AST (work by François Poulain, project DoCoq)Gravatar Enrico Tassi2014-09-29
* Notation: option to attach extra pretty printing rules to notationsGravatar Enrico Tassi2014-09-29
* CoqIDE: new message to print ASTGravatar Enrico Tassi2014-09-29
* typoGravatar Enrico Tassi2014-09-29
* do not explode if a plugin is not up to date on -help (Close: 3673)Gravatar Enrico Tassi2014-09-29
* Merging some functions from evarutil.ml/evd.ml.Gravatar Hugo Herbelin2014-09-29
* Printing evar instance in a more intuitive order.Gravatar Hugo Herbelin2014-09-29
* Restoring non-uniform delta on local and global constants in 2nd orderGravatar Hugo Herbelin2014-09-29
* Documenting option -type-in-type.Gravatar Hugo Herbelin2014-09-29
* Adding a test for bug #2428.Gravatar Pierre-Marie Pédrot2014-09-29
* Bug fixed.Gravatar Matthieu Sozeau2014-09-29
* Fix test-suite filesGravatar Matthieu Sozeau2014-09-29
* Fix printing of primitive record info.Gravatar Matthieu Sozeau2014-09-29
* In evarconv and unification, expand folded primitive projections toGravatar Matthieu Sozeau2014-09-29
* Print information about primitive records (Print and About).Gravatar Matthieu Sozeau2014-09-28
* Keyed unification option, compiling the whole standard libraryGravatar Matthieu Sozeau2014-09-27
* Index keys instead of simply global references.Gravatar Matthieu Sozeau2014-09-27
* First version of keyed subterm selection in unification.Gravatar Matthieu Sozeau2014-09-27
* Fix test-suite file.Gravatar Matthieu Sozeau2014-09-27
* Fix bug #3664 by refolding projections that don't reduce in cbn.Gravatar Matthieu Sozeau2014-09-27
* Remove auto's use of dummy goal, use the proper sigma for pattern_of_constr.Gravatar Matthieu Sozeau2014-09-27
* Fix semantics of matching with folded/unfolded projections to definitelyGravatar Matthieu Sozeau2014-09-27
* Fix bug #3672, application of primitive projections as coercions.Gravatar Matthieu Sozeau2014-09-27
* Fix bug 3662 by actually reducing primitive projections in cbv/compute.Gravatar Matthieu Sozeau2014-09-27
* Bug fixed.Gravatar Matthieu Sozeau2014-09-27
* Make pattern_of_constr typed so that we can infer the proper patternsGravatar Matthieu Sozeau2014-09-27
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Adapting to naming of evars.Gravatar Hugo Herbelin2014-09-27
* Changed semantics of induction !id when a clause is given: don'tGravatar Hugo Herbelin2014-09-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 20:12:16 +0000