| Commit message (Expand) | Author | Age |
* | Remove dead code. | Maxime Dénès | 2015-01-17 |
* | Univs: proper printing of global and local universe names (only | Matthieu Sozeau | 2015-01-17 |
* | Partially revert "Forbid Require inside interactive modules and module types." | Maxime Dénès | 2015-01-17 |
* | Avoid compilation warning... might not be the best fix though. | Matthieu Sozeau | 2015-01-17 |
* | Made -print-mod-uid more silent and robust. | Maxime Dénès | 2015-01-13 |
* | Fix bug when discharging universe constraints coming from variables | Matthieu Sozeau | 2015-01-13 |
* | fixup to vi -> vio renaming | Enrico Tassi | 2015-01-12 |
* | Update headers. | Maxime Dénès | 2015-01-12 |
* | Declarations.mli refactoring: module_type_body = module_body | Pierre Letouzey | 2015-01-11 |
* | kernel/ind Change interface of declare_mind and declare_mutual | Matthieu Sozeau | 2015-01-05 |
* | Forbid Require inside interactive modules and module types. | Maxime Dénès | 2014-12-25 |
* | Summary: more surgery functions | Enrico Tassi | 2014-12-17 |
* | Global: export the name of the summary entry | Enrico Tassi | 2014-12-17 |
* | Getting rid of Exninfo hacks. | Pierre-Marie Pédrot | 2014-12-16 |
* | Fix for #3154: use CUnix.sys_command to call native compiler. | Maxime Dénès | 2014-12-16 |
* | Switch the few remaining iso-latin-1 files to utf8 | Pierre Letouzey | 2014-12-09 |
* | Reverting the following block of three commits: | Hugo Herbelin | 2014-11-27 |
* | Registering strict implicit arguments systematically. | Hugo Herbelin | 2014-11-26 |
* | Pass around information on the use of template polymorphism for | Matthieu Sozeau | 2014-11-23 |
* | Universes.nf_evars_and_universes_opt_subst substitutes evars eagerly. | Pierre-Marie Pédrot | 2014-11-10 |
* | Better error messages when unfreezing summary entries | Enrico Tassi | 2014-10-30 |
* | When loading libraries, feed back dependencies. | Carst Tankink | 2014-10-13 |
* | STM: primitives to snapshot a .vi while in interactive mode | Enrico Tassi | 2014-10-13 |
* | selective join/export of the safe_environment | Enrico Tassi | 2014-10-13 |
* | STM: simplify how the term part of a side effect is retrieved | Enrico Tassi | 2014-10-13 |
* | library/opaqueTables: enable their use in interactive mode | Enrico Tassi | 2014-10-13 |
* | Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name | Matthieu Sozeau | 2014-10-11 |
* | Keyed unification option, compiling the whole standard library | Matthieu Sozeau | 2014-09-27 |
* | Index keys instead of simply global references. | Matthieu Sozeau | 2014-09-27 |
* | First version of keyed subterm selection in unification. | Matthieu Sozeau | 2014-09-27 |
* | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau | 2014-09-27 |
* | Make eq_pattern_test/eq_test work up to the equivalence of primitive | Matthieu Sozeau | 2014-09-24 |
* | Providing a -type-in-type option for collapsing the universe hierarchy. | Hugo Herbelin | 2014-09-13 |
* | Parsing and printing of primitive projections, fix buggy behavior when | Matthieu Sozeau | 2014-09-10 |
* | - Fix printing and parsing of primitive projections, including the Set | Matthieu Sozeau | 2014-09-09 |
* | Removing dead code relative to the XML plugin. | Pierre-Marie Pédrot | 2014-09-08 |
* | Print [Variant] types with the keyword [Variant]. | Arnaud Spiwack | 2014-09-04 |
* | Fixing bug #2818. | Pierre-Marie Pédrot | 2014-09-03 |
* | Fix Declaremods.end_library (Closes: #3536) | Enrico Tassi | 2014-09-02 |
* | Simplify even further the declaration of primitive projections, | Matthieu Sozeau | 2014-08-30 |
* | Change the way primitive projections are declared to the kernel. | Matthieu Sozeau | 2014-08-28 |
* | Fix computation of dangling constraints at the end of a proof (bug #3531). | Matthieu Sozeau | 2014-08-25 |
* | instanciation is French, instantiation is English | Jason Gross | 2014-08-25 |
* | Grammar: "avoiding to" isn't proper, either | Jason Gross | 2014-08-25 |
* | Small code simplification. | Pierre-Marie Pédrot | 2014-08-05 |
* | Move to a representation of universe polymorphic constants using indices for ... | Matthieu Sozeau | 2014-08-03 |
* | - Do module substitution inside mind_record. | Matthieu Sozeau | 2014-07-25 |
* | More straightforward definition of Universes.add_list_map. | Pierre-Marie Pédrot | 2014-07-21 |
* | Cleanup substitution inside universe instances, only done through subst_fn now, | Matthieu Sozeau | 2014-07-21 |
* | Unifying locate code, also making it more powerful: it is now able to find | Pierre-Marie Pédrot | 2014-07-21 |