aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* Parsing of Type@{max(i,j)}.Gravatar Matthieu Sozeau2014-09-08
* Fixing bug #3492.Gravatar Pierre-Marie Pédrot2014-09-07
* Renaming goal-entering functions.Gravatar Pierre-Marie Pédrot2014-09-06
* More explicit printing in Himsg.Gravatar Pierre-Marie Pédrot2014-09-04
* Commands like [Inductive > X := … | … | …] raise an error message inste...Gravatar Arnaud Spiwack2014-09-04
* Remove [Infer] option of records.Gravatar Arnaud Spiwack2014-09-04
* Type definitions with [Variant] don't generate inductive schemes by default.Gravatar Arnaud Spiwack2014-09-04
* Type definitions [Variant] and [Record] really don't accept the wrong kind of...Gravatar Arnaud Spiwack2014-09-04
* Types declared as Variants really do not accept recursive definitions.Gravatar Arnaud Spiwack2014-09-04
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
* Print error messages with more hidden information based on α-equivalence .Gravatar Arnaud Spiwack2014-09-03
* Additional entry tactic_arg in Print Grammar tactic.Gravatar Pierre-Marie Pédrot2014-09-03
* coqworkmgrGravatar Enrico Tassi2014-09-02
* Getting rid of atomic tactics in Tacenv.Gravatar Pierre-Marie Pédrot2014-08-31
* Moving code of tactic interpretation from Tacenv to Vernacentries.Gravatar Pierre-Marie Pédrot2014-08-31
* Simplify even further the declaration of primitive projections,Gravatar Matthieu Sozeau2014-08-30
* Fixing commit 50237af2.Gravatar Pierre-Marie Pédrot2014-08-29
* Fix bug when defining primitive projections mixing defined and abstracts fields.Gravatar Matthieu Sozeau2014-08-29
* Fixing bug #3528.Gravatar Pierre-Marie Pédrot2014-08-28
* Change the way primitive projections are declared to the kernel.Gravatar Matthieu Sozeau2014-08-28
* Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possibleGravatar Matthieu Sozeau2014-08-25
* Fixing the essence of naming bug #3204: use same strategy for namingGravatar Hugo Herbelin2014-08-25
* Prerequisite to fix stm test-suite when not in -localGravatar Pierre Boutillier2014-08-25
* Fixing bug #3533.Gravatar Pierre-Marie Pédrot2014-08-23
* Move UnsatisfiableConstraints to a pretype error.Gravatar Matthieu Sozeau2014-08-22
* Reorganisation of intropattern codeGravatar Hugo Herbelin2014-08-18
* Reorganization of tactics:Gravatar Hugo Herbelin2014-08-18
* Moving the TacAlias node out of atomic tactics.Gravatar Pierre-Marie Pédrot2014-08-18
* Moving the TacExtend node from atomic to plain tactics.Gravatar Pierre-Marie Pédrot2014-08-18
* Removing documentation related to the deprecated State machinery.Gravatar Pierre-Marie Pédrot2014-08-16
* Fix program using an the unsubstituted type of the original obligationGravatar Matthieu Sozeau2014-08-14
* Bettre pretty-printing of evar maps, avoids printing universe informationGravatar Matthieu Sozeau2014-08-13
* Fixing parsing of bullets after a "...".Gravatar Hugo Herbelin2014-08-12
* Better structure for Ltac pretyping environments.Gravatar Pierre-Marie Pédrot2014-08-07
* [uconstr]: use a closure instead of eager substitution.Gravatar Arnaud Spiwack2014-08-06
* Experimentally adding an option for automatically erasing anGravatar Hugo Herbelin2014-08-05
* STM: new "par:" goal selector, like "all:" but in parallelGravatar Enrico Tassi2014-08-05
* STM: code restructured to reuse task queue for tacticsGravatar Enrico Tassi2014-08-05
* Cleaning of the new implementation of the tactic monad.Gravatar Arnaud Spiwack2014-08-04
* Fix infer conv using the wrong universe conversion flexibility informationGravatar Matthieu Sozeau2014-08-03
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* Fix bug #3453, not recognizing primitive projections in Coercion declarations.Gravatar Matthieu Sozeau2014-07-29
* Qualified ML tactic names. The plugin name is used to discriminateGravatar Pierre-Marie Pédrot2014-07-27
* - Do module substitution inside mind_record.Gravatar Matthieu Sozeau2014-07-25
* Refined guard condition of cofixpoints, to anticipate potential futurGravatar Maxime Dénès2014-07-22
* First attempt at a fix for guard condition on cofixpoints.Gravatar Maxime Dénès2014-07-22
* Unifying locate code, also making it more powerful: it is now able to findGravatar Pierre-Marie Pédrot2014-07-21
* Adding a new "Locate Term" command, distinct from the raw "Locate" command.Gravatar Pierre-Marie Pédrot2014-07-21
* More complete printing of Ltac location, akin to the term-dedicated Locate co...Gravatar Pierre-Marie Pédrot2014-07-21
* - Fix bug introduced in obligations which wouldn't consider all evars that areGravatar Matthieu Sozeau2014-07-16