| Age | Commit message (Expand) | Author |
|---|
| 2014-08-25 | Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possible | Matthieu Sozeau |
| 2014-08-25 | Fixing the essence of naming bug #3204: use same strategy for naming | Hugo Herbelin |
| 2014-08-25 | Prerequisite to fix stm test-suite when not in -local | Pierre Boutillier |
| 2014-08-23 | Fixing bug #3533. | Pierre-Marie Pédrot |
| 2014-08-22 | Move UnsatisfiableConstraints to a pretype error. | Matthieu Sozeau |
| 2014-08-18 | Reorganisation of intropattern code | Hugo Herbelin |
| 2014-08-18 | Reorganization of tactics: | Hugo Herbelin |
| 2014-08-18 | Moving the TacAlias node out of atomic tactics. | Pierre-Marie Pédrot |
| 2014-08-18 | Moving the TacExtend node from atomic to plain tactics. | Pierre-Marie Pédrot |
| 2014-08-16 | Removing documentation related to the deprecated State machinery. | Pierre-Marie Pédrot |
| 2014-08-14 | Fix program using an the unsubstituted type of the original obligation | Matthieu Sozeau |
| 2014-08-13 | Bettre pretty-printing of evar maps, avoids printing universe information | Matthieu Sozeau |
| 2014-08-12 | Fixing parsing of bullets after a "...". | Hugo Herbelin |
| 2014-08-07 | Better structure for Ltac pretyping environments. | Pierre-Marie Pédrot |
| 2014-08-06 | [uconstr]: use a closure instead of eager substitution. | Arnaud Spiwack |
| 2014-08-05 | Experimentally adding an option for automatically erasing an | Hugo Herbelin |
| 2014-08-05 | STM: new "par:" goal selector, like "all:" but in parallel | Enrico Tassi |
| 2014-08-05 | STM: code restructured to reuse task queue for tactics | Enrico Tassi |
| 2014-08-04 | Cleaning of the new implementation of the tactic monad. | Arnaud Spiwack |
| 2014-08-03 | Fix infer conv using the wrong universe conversion flexibility information | Matthieu Sozeau |
| 2014-08-03 | Move to a representation of universe polymorphic constants using indices for ... | Matthieu Sozeau |
| 2014-07-29 | Fix bug #3453, not recognizing primitive projections in Coercion declarations. | Matthieu Sozeau |
| 2014-07-27 | Qualified ML tactic names. The plugin name is used to discriminate | Pierre-Marie Pédrot |
| 2014-07-25 | - Do module substitution inside mind_record. | Matthieu Sozeau |
| 2014-07-22 | Refined guard condition of cofixpoints, to anticipate potential futur | Maxime Dénès |
| 2014-07-22 | First attempt at a fix for guard condition on cofixpoints. | Maxime Dénès |
| 2014-07-21 | Unifying locate code, also making it more powerful: it is now able to find | Pierre-Marie Pédrot |
| 2014-07-21 | Adding a new "Locate Term" command, distinct from the raw "Locate" command. | Pierre-Marie Pédrot |
| 2014-07-21 | More 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 are | Matthieu Sozeau |
| 2014-07-14 | smartlocate: look for the head symbol for real | Enrico Tassi |
| 2014-07-13 | Adding a "time" tactical for benchmarking purposes. In case the tactic | Hugo Herbelin |
| 2014-07-11 | Properly add a Set lower bound on any polymorphic inductive in Type with | Matthieu Sozeau |
| 2014-07-11 | STM: let toploop plugins specify the flags for STM workers | Enrico Tassi |
| 2014-07-11 | STM: flag to turn off branch reopening | Enrico Tassi |
| 2014-07-11 | Feedback: LoadedFile + Goals | Enrico Tassi |
| 2014-07-10 | Better handling of the universe context in case of Admitted proof obligations. | Matthieu Sozeau |
| 2014-07-10 | option to always delegate futures to workers | Enrico Tassi |
| 2014-07-09 | Arith: full integration of the "Numbers" modular framework | Pierre Letouzey |
| 2014-07-07 | Revert "time tac" (committed by mistake). | Hugo Herbelin |
| 2014-07-07 | time tac | Hugo Herbelin |
| 2014-07-03 | Cleanup code related to the constraint solving, which sits now outside the | Matthieu Sozeau |
| 2014-07-03 | Properly compute the transitive closure of the system of constraints | Matthieu Sozeau |
| 2014-07-03 | When defining a monomorphic Program, do not allow arbitrary instantiations | Matthieu Sozeau |
| 2014-07-01 | Add toplevel commands to declare global universes and constraints. | Matthieu Sozeau |
| 2014-07-01 | Making code and doc agree on "Set Equality Schemes" (see also bug #2550). | Hugo Herbelin |
| 2014-07-01 | Fixing the place where to insert a space in "Tactic failure" | Hugo Herbelin |
| 2014-07-01 | More informative message when Mltop.load_object fails. | Hugo Herbelin |
| 2014-06-30 | Useless keeping of dirpath in tactic aliases. | Pierre-Marie Pédrot |
| 2014-06-28 | Moved code for finding subterms (pattern, induction, set, generalize, ...) | Hugo Herbelin |
