aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Expand)AuthorAge
* Documenting option -type-in-type.Gravatar Hugo Herbelin2014-09-29
* Fixing inversion after having fixed intros_replacingGravatar Hugo Herbelin2014-09-10
* Documenting the new Undo semanticsGravatar Enrico Tassi2014-09-09
* Removing the documentation of the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
* CHANGES: existential variables are always "substituted" in the new tactic eng...Gravatar Arnaud Spiwack2014-09-08
* CHANGES: Ltac's [refine] accepts [uconstr].Gravatar Arnaud Spiwack2014-09-08
* CHANGES: [revgoals].Gravatar Arnaud Spiwack2014-09-08
* CHANGES: [Variant], [Set Nonrecursive Elimination Schemes].Gravatar Arnaud Spiwack2014-09-08
* CHANGES: binder names from Ltac identifiers.Gravatar Arnaud Spiwack2014-09-08
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* Grammar: "allowing to" is not proper EnglishGravatar Jason Gross2014-08-25
* Adding a new intro-pattern for "apply in" on the fly. Using syntaxGravatar Hugo Herbelin2014-08-18
* Uncountably many bullets (+,-,*,++,--,**,+++,...).Gravatar Hugo Herbelin2014-08-05
* Experimentally adding an option for automatically erasing anGravatar Hugo Herbelin2014-08-05
* Adding a syntax "enough" for the variant of "assert" with the order ofGravatar Hugo Herbelin2014-08-05
* A new step in the new "standard" naming policy for propositional hypothesesGravatar Hugo Herbelin2014-08-05
* CHANGES: [>…].Gravatar Arnaud Spiwack2014-08-01
* CHANGES: [numgoals] and [guard].Gravatar Arnaud Spiwack2014-08-01
* Making the error message about bullets more precise.Gravatar Pierre Courtieu2014-07-31
* CHANGES: untyped terms in tacticsGravatar Arnaud Spiwack2014-07-29
* CHANGES: cycle and swap.Gravatar Arnaud Spiwack2014-07-25
* CHANGES: yellow in Coqide.Gravatar Arnaud Spiwack2014-07-25
* CHANGE: add Derive.Gravatar Arnaud Spiwack2014-07-25
* CHANGE: document the features of the new tactic engine.Gravatar Arnaud Spiwack2014-07-25
* Documenting the changes of Locate semantics.Gravatar Pierre-Marie Pédrot2014-07-21
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 07:01:07 +0000