aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Expand)AuthorAge
* Documenting the need of the "DECLARE PLUGIN" statement.Gravatar Pierre-Marie Pédrot2014-07-21
* Documenting the change of semantics of the "constructor" tactic.Gravatar Pierre-Marie Pédrot2014-07-21
* Mentioning the incompatibility due to fixing bug #2996 (see #3418).Gravatar Hugo Herbelin2014-07-13
* Adding a "time" tactical for benchmarking purposes. In case the tacticGravatar Hugo Herbelin2014-07-13
* Synchronized names from the "as" clause with the skeleton of theGravatar Hugo Herbelin2014-06-30
* Updating CHANGES w.r.t. opacity in type inference + layout of file.Gravatar Hugo Herbelin2014-06-28
* Add some compatibility notes on the changes to [change] and unification in ge...Gravatar Matthieu Sozeau2014-06-23
* Use of "H"-based names for propositional hypotheses obtained byGravatar Hugo Herbelin2014-06-01
* More on injection over a projectable "existT". - Fixing syntax "injection ......Gravatar Hugo Herbelin2014-05-31
* Restored old behavior of injection on proofs by default.Gravatar Maxime Dénès2014-05-18
* More documentation of new features in CHANGE.Gravatar Pierre-Marie Pédrot2014-05-09
* Simplification and improvement of "subst x" in such a way that itGravatar Hugo Herbelin2014-05-08
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Document changes on injection.Gravatar Maxime Dénès2014-04-30
* Revert "Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with...Gravatar Pierre Boutillier2014-04-09
* Add an option -Q (tentative name).Gravatar Guillaume Melquiond2014-04-08
* Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with -R. (Fi...Gravatar Guillaume Melquiond2014-04-07
* Change handling of loadpath and mlpath.Gravatar Guillaume Melquiond2014-04-06
* Coqmktop without Sys.command, changes in ./configure -*byteflags optionsGravatar Pierre Letouzey2014-01-30
* More in CHANGES.Gravatar Pierre-Marie Pédrot2014-01-25
* Omega: avoiding distinct proof-terms on repeated identical runsGravatar Pierre Letouzey2014-01-10
* Documenting the tactic-in-term construction.Gravatar Pierre-Marie Pédrot2013-12-11
* Change in vo format : digest aren't Marshalled anymoreGravatar letouzey2013-08-22
* Revising r16550 about providing intro patterns for applying injection:Gravatar herbelin2013-07-09
* Document changes and add missing documentation for Program options.Gravatar msozeau2013-06-06
* Making the behavior of "injection ... as ..." more natural:Gravatar herbelin2013-06-02
* Now interpreting introduction patterns [x1 .. xn] and (x1,..,xn) as anGravatar herbelin2013-06-02
* Documenting the "appcontext" by default.Gravatar ppedrot2013-05-29
* "change ... in ..." and "simpl ... in ..." now consider nestedGravatar herbelin2013-05-14
* Reporting the change on matching partial applications in patterns ofGravatar herbelin2013-05-05
* Renaming SearchAbout into Search and Search into SearchHead.Gravatar herbelin2013-04-17
* Using hnf instead of "intro H" for forcing reduction to a product.Gravatar herbelin2013-03-21
* Fixing an old pecularity of "red": head betaiota redexes are nowGravatar herbelin2013-03-21
* Allowing (Co)Fixpoint to be defined local and Let-style.Gravatar ppedrot2013-03-11
* Added a Local Definition vernacular command. This type of definitionGravatar ppedrot2013-03-11
* Displaying environment and unfolding aliases in "cannot_unify"Gravatar herbelin2013-02-17
* Revised the strategy for automatic insertion of spaces when printingGravatar herbelin2012-12-04
* CHANGES: document the end of states/initial.coq and coqtop.optGravatar letouzey2012-08-23
* Added support for option Local (at module level) in Tactic Notation.Gravatar herbelin2012-08-11
* Some changes in CHANGES.Gravatar herbelin2012-08-11
* Cleaning CHANGES consistently with v8.4. Documenting COMPATIBILITY.Gravatar herbelin2012-08-08
* Document the command Add/Remove Search BlacklistGravatar letouzey2012-08-03
* re-sync CHANGES with 8.4Gravatar letouzey2012-08-03
* The tactic remember now accepts a final eqn:H option (grant wish #2489)Gravatar letouzey2012-07-09
* induction/destruct : nicer syntax for generating equations (solves #2741)Gravatar letouzey2012-07-09
* Quick update to CHANGES, mention especially the new parsing of ->Gravatar letouzey2012-07-05
* CHANGES: mention the end of induction principles for recordsGravatar letouzey2012-06-05
* Some documentation of recent changes concerning interfacesGravatar letouzey2012-05-29
* CHANGES: fix a typo + an entry in the wrong sectionGravatar letouzey2012-05-23
* Intuition: temporary(?) restore the unconditional unfolding of notGravatar letouzey2012-05-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 20:05:08 +0000