| Age | Commit message (Expand) | Author |
|---|
| 2015-01-05 | kernel/ind Change interface of declare_mind and declare_mutual | Matthieu Sozeau |
| 2014-12-25 | Forbid Require inside interactive modules and module types. | Maxime Dénès |
| 2014-12-17 | Summary: more surgery functions | Enrico Tassi |
| 2014-12-17 | Global: export the name of the summary entry | Enrico Tassi |
| 2014-12-16 | 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-09 | Switch the few remaining iso-latin-1 files to utf8 | Pierre Letouzey |
| 2014-11-27 | Reverting the following block of three commits: | Hugo Herbelin |
| 2014-11-26 | Registering strict implicit arguments systematically. | Hugo Herbelin |
| 2014-11-23 | Pass around information on the use of template polymorphism for | Matthieu Sozeau |
| 2014-11-10 | Universes.nf_evars_and_universes_opt_subst substitutes evars eagerly. | Pierre-Marie Pédrot |
| 2014-10-30 | Better error messages when unfreezing summary entries | Enrico Tassi |
| 2014-10-13 | 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-11 | Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name | Matthieu Sozeau |
| 2014-09-27 | 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-24 | Make eq_pattern_test/eq_test work up to the equivalence of primitive | Matthieu Sozeau |
| 2014-09-13 | Providing a -type-in-type option for collapsing the universe hierarchy. | Hugo Herbelin |
| 2014-09-10 | Parsing and printing of primitive projections, fix buggy behavior when | Matthieu Sozeau |
| 2014-09-09 | - Fix printing and parsing of primitive projections, including the Set | Matthieu Sozeau |
| 2014-09-08 | Removing dead code relative to the XML plugin. | Pierre-Marie Pédrot |
| 2014-09-04 | Print [Variant] types with the keyword [Variant]. | Arnaud Spiwack |
| 2014-09-03 | Fixing bug #2818. | Pierre-Marie Pédrot |
| 2014-09-02 | Fix Declaremods.end_library (Closes: #3536) | Enrico Tassi |
| 2014-08-30 | Simplify even further the declaration of primitive projections, | Matthieu Sozeau |
| 2014-08-28 | Change the way primitive projections are declared to the kernel. | Matthieu Sozeau |
| 2014-08-25 | 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-05 | Small code simplification. | Pierre-Marie Pédrot |
| 2014-08-03 | Move to a representation of universe polymorphic constants using indices for ... | Matthieu Sozeau |
| 2014-07-25 | - Do module substitution inside mind_record. | Matthieu Sozeau |
| 2014-07-21 | 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 | 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-11 | Feedback: LoadedFile + Goals | Enrico Tassi |
| 2014-07-03 | Cleanup code related to the constraint solving, which sits now outside the | Matthieu Sozeau |
| 2014-07-01 | Add toplevel commands to declare global universes and constraints. | Matthieu Sozeau |
| 2014-06-25 | all coqide specific files moved into ide/ | Enrico Tassi |
| 2014-06-21 | When discharging polymorphic definitions, we must take into account all | Matthieu Sozeau |
| 2014-06-20 | Fixed some HoTT bugs, provide a proper error message when giving an ill-formed | Matthieu Sozeau |
| 2014-06-18 | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau |
