aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2014-09-04Commands like [Inductive > X := … | … | …] raise an error message inste...Arnaud Spiwack
2014-09-04Remove [Infer] option of records.Arnaud Spiwack
2014-09-04Type definitions with [Variant] don't generate inductive schemes by default.Arnaud Spiwack
2014-09-04Type definitions [Variant] and [Record] really don't accept the wrong kind of...Arnaud Spiwack
2014-09-04Types declared as Variants really do not accept recursive definitions.Arnaud Spiwack
2014-09-04Print [Variant] types with the keyword [Variant].Arnaud Spiwack
2014-09-03Print error messages with more hidden information based on α-equivalence .Arnaud Spiwack
2014-09-03Additional entry tactic_arg in Print Grammar tactic.Pierre-Marie Pédrot
2014-09-02coqworkmgrEnrico Tassi
2014-08-31Getting rid of atomic tactics in Tacenv.Pierre-Marie Pédrot
2014-08-31Moving code of tactic interpretation from Tacenv to Vernacentries.Pierre-Marie Pédrot
2014-08-30Simplify even further the declaration of primitive projections,Matthieu Sozeau
2014-08-29Fixing commit 50237af2.Pierre-Marie Pédrot
2014-08-29Fix bug when defining primitive projections mixing defined and abstracts fields.Matthieu Sozeau
2014-08-28Fixing bug #3528.Pierre-Marie Pédrot
2014-08-28Change the way primitive projections are declared to the kernel.Matthieu Sozeau
2014-08-25Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possibleMatthieu Sozeau
2014-08-25Fixing the essence of naming bug #3204: use same strategy for namingHugo Herbelin
2014-08-25Prerequisite to fix stm test-suite when not in -localPierre Boutillier
2014-08-23Fixing bug #3533.Pierre-Marie Pédrot
2014-08-22Move UnsatisfiableConstraints to a pretype error.Matthieu Sozeau
2014-08-18Reorganisation of intropattern codeHugo Herbelin
2014-08-18Reorganization of tactics:Hugo Herbelin
2014-08-18Moving the TacAlias node out of atomic tactics.Pierre-Marie Pédrot
2014-08-18Moving the TacExtend node from atomic to plain tactics.Pierre-Marie Pédrot
2014-08-16Removing documentation related to the deprecated State machinery.Pierre-Marie Pédrot
2014-08-14Fix program using an the unsubstituted type of the original obligationMatthieu Sozeau
2014-08-13Bettre pretty-printing of evar maps, avoids printing universe informationMatthieu Sozeau
2014-08-12Fixing parsing of bullets after a "...".Hugo Herbelin
2014-08-07Better structure for Ltac pretyping environments.Pierre-Marie Pédrot
2014-08-06[uconstr]: use a closure instead of eager substitution.Arnaud Spiwack
2014-08-05Experimentally adding an option for automatically erasing anHugo Herbelin
2014-08-05STM: new "par:" goal selector, like "all:" but in parallelEnrico Tassi
2014-08-05STM: code restructured to reuse task queue for tacticsEnrico Tassi
2014-08-04Cleaning of the new implementation of the tactic monad.Arnaud Spiwack
2014-08-03Fix infer conv using the wrong universe conversion flexibility informationMatthieu Sozeau
2014-08-03Move to a representation of universe polymorphic constants using indices for ...Matthieu Sozeau
2014-07-29Fix bug #3453, not recognizing primitive projections in Coercion declarations.Matthieu Sozeau
2014-07-27Qualified ML tactic names. The plugin name is used to discriminatePierre-Marie Pédrot
2014-07-25- Do module substitution inside mind_record.Matthieu Sozeau
2014-07-22Refined guard condition of cofixpoints, to anticipate potential futurMaxime Dénès
2014-07-22First attempt at a fix for guard condition on cofixpoints.Maxime Dénès
2014-07-21Unifying locate code, also making it more powerful: it is now able to findPierre-Marie Pédrot
2014-07-21Adding a new "Locate Term" command, distinct from the raw "Locate" command.Pierre-Marie Pédrot
2014-07-21More complete printing of Ltac location, akin to the term-dedicated Locate co...Pierre-Marie Pédrot
2014-07-16- Fix bug introduced in obligations which wouldn't consider all evars that areMatthieu Sozeau
2014-07-14smartlocate: look for the head symbol for realEnrico Tassi
2014-07-13Adding a "time" tactical for benchmarking purposes. In case the tacticHugo Herbelin
2014-07-11Properly add a Set lower bound on any polymorphic inductive in Type withMatthieu Sozeau
2014-07-11STM: let toploop plugins specify the flags for STM workersEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-01 00:58:38 +0000