| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot |
| 2014-06-17 | - Fix the de Bruijn problem in check_projection for good :) | Matthieu Sozeau |
| 2014-06-17 | Safer entry point of primitive projections in the kernel, now it does recognize | Matthieu Sozeau |
| 2014-06-16 | Checking that a library name is valid before compilation. | Pierre-Marie Pédrot |
| 2014-06-13 | Deprecate options -dont, -lazy, -force-load-proofs. | Guillaume Melquiond |
| 2014-06-13 | Less ocaml warnings. | Hugo Herbelin |
| 2014-06-10 | - 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-08 | ind_tables: always declare side effects (Closes: HOTT#110) | Enrico Tassi |
| 2014-06-08 | Function in Univ uselessly exported. | Pierre-Marie Pédrot |
| 2014-06-04 | - Fix hashing of levels to get the "right" order in universe contexts etc... | Matthieu Sozeau |
| 2014-05-22 | Fix native_compute for systems with a limited size for the command line. | Guillaume Melquiond |
