| Commit message (Expand) | Author | Age |
* | More complete printing of Ltac location, akin to the term-dedicated Locate co... | Pierre-Marie Pédrot | 2014-07-21 |
* | - Fix bug introduced in obligations which wouldn't consider all evars that are | Matthieu Sozeau | 2014-07-16 |
* | smartlocate: look for the head symbol for real | Enrico Tassi | 2014-07-14 |
* | Adding a "time" tactical for benchmarking purposes. In case the tactic | Hugo Herbelin | 2014-07-13 |
* | 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-11 |
* | 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-10 |
* | Arith: full integration of the "Numbers" modular framework | Pierre Letouzey | 2014-07-09 |
* | Revert "time tac" (committed by mistake). | Hugo Herbelin | 2014-07-07 |
* | time tac | Hugo Herbelin | 2014-07-07 |
* | 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-03 |
* | 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-07-01 |
* | Useless keeping of dirpath in tactic aliases. | Pierre-Marie Pédrot | 2014-06-30 |
* | Moved code for finding subterms (pattern, induction, set, generalize, ...) | Hugo Herbelin | 2014-06-28 |
* | Made the subterm finding function make_abstraction independent of the | Hugo Herbelin | 2014-06-28 |
* | all coqide specific files moved into ide/ | Enrico Tassi | 2014-06-25 |
* | cut toploop(s) out of coqtop: now they are loaded dynamically | Enrico Tassi | 2014-06-25 |
* | Fix computation of Type argument for Program's fix_proto. | Matthieu Sozeau | 2014-06-24 |
* | Proper handling of the polymorphism flag for Context, fixing HoTT bug #98. | Matthieu Sozeau | 2014-06-23 |
* | Cleanup treatment of template universe polymorphism (thanks to E. Tassi | Matthieu Sozeau | 2014-06-20 |
* | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau | 2014-06-18 |
* | Adapt coercion code to work with projections as target classes. | Matthieu Sozeau | 2014-06-17 |
* | Complying an ocaml warning. | Hugo Herbelin | 2014-06-17 |
* | Removing dead code. | Pierre-Marie Pédrot | 2014-06-17 |
* | Safer entry point of primitive projections in the kernel, now it does recognize | Matthieu Sozeau | 2014-06-17 |
* | - Add "Show Universes" to print information about universes during a proof. | Matthieu Sozeau | 2014-06-16 |
* | Fix spacing in error message. | Guillaume Melquiond | 2014-06-16 |
* | Deprecate useless option -quality. | Guillaume Melquiond | 2014-06-13 |
* | Remove documentation for the unsupported options -byte and -opt. | Guillaume Melquiond | 2014-06-13 |
* | Deprecate useless option -unsafe. | Guillaume Melquiond | 2014-06-13 |
* | Deprecate options -dont, -lazy, -force-load-proofs. | Guillaume Melquiond | 2014-06-13 |
* | Improved error message when a meta posed as an evar remains unsolved | Hugo Herbelin | 2014-06-13 |
* | Fix bug #3289 | Matthieu Sozeau | 2014-06-11 |
* | - Fix substitution of universes which needlessly hashconsed existing universes. | Matthieu Sozeau | 2014-06-10 |
* | Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un... | Matthieu Sozeau | 2014-06-10 |
* | Adding a toplevel option allowing to deactivate the term sharing in kernel | Pierre-Marie Pédrot | 2014-06-08 |
* | Moving hook code from Future to Lemmas. This seemed to disrupt compilation of | Pierre-Marie Pédrot | 2014-06-08 |
* | Enforce a correct exception handling in declaration_hooks | Enrico Tassi | 2014-06-08 |
* | ind_tables: always declare side effects (Closes: HOTT#110) | Enrico Tassi | 2014-06-08 |
* | Adding a new Control file centralizing the control options of Coq. | Pierre-Marie Pédrot | 2014-06-07 |
* | Remove the syntax [Vernac1. Vernac2. … Vernacn. ]. | Arnaud Spiwack | 2014-06-06 |
* | Collecting in Namegen those conventional default names that are used in diffe... | Hugo Herbelin | 2014-06-04 |