aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* 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
* smartlocate: look for the head symbol for realGravatar Enrico Tassi2014-07-14
* Adding a "time" tactical for benchmarking purposes. In case the tacticGravatar Hugo Herbelin2014-07-13
* Properly add a Set lower bound on any polymorphic inductive in Type withGravatar Matthieu Sozeau2014-07-11
* STM: let toploop plugins specify the flags for STM workersGravatar Enrico Tassi2014-07-11
* STM: flag to turn off branch reopeningGravatar Enrico Tassi2014-07-11
* Feedback: LoadedFile + GoalsGravatar Enrico Tassi2014-07-11
* Better handling of the universe context in case of Admitted proof obligations.Gravatar Matthieu Sozeau2014-07-10
* option to always delegate futures to workersGravatar Enrico Tassi2014-07-10
* Arith: full integration of the "Numbers" modular frameworkGravatar Pierre Letouzey2014-07-09
* Revert "time tac" (committed by mistake).Gravatar Hugo Herbelin2014-07-07
* time tacGravatar Hugo Herbelin2014-07-07
* Cleanup code related to the constraint solving, which sits now outside theGravatar Matthieu Sozeau2014-07-03
* Properly compute the transitive closure of the system of constraintsGravatar Matthieu Sozeau2014-07-03
* When defining a monomorphic Program, do not allow arbitrary instantiationsGravatar Matthieu Sozeau2014-07-03
* Add toplevel commands to declare global universes and constraints.Gravatar Matthieu Sozeau2014-07-01
* Making code and doc agree on "Set Equality Schemes" (see also bug #2550).Gravatar Hugo Herbelin2014-07-01
* Fixing the place where to insert a space in "Tactic failure"Gravatar Hugo Herbelin2014-07-01
* More informative message when Mltop.load_object fails.Gravatar Hugo Herbelin2014-07-01
* Useless keeping of dirpath in tactic aliases.Gravatar Pierre-Marie Pédrot2014-06-30
* Moved code for finding subterms (pattern, induction, set, generalize, ...)Gravatar Hugo Herbelin2014-06-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 02:38:29 +0000