| Age | Commit message (Expand) | Author |
|---|
| 2014-09-30 | Add syntax for naming new goals in refine: writing ?[id] instead of _ | Hugo Herbelin |
| 2014-09-29 | Merging some functions from evarutil.ml/evd.ml. | Hugo Herbelin |
| 2014-09-24 | Rename eq_constr functions in Evd to not break backward compatibility | Matthieu Sozeau |
| 2014-09-17 | Be more conservative and keep the use of eq_constr in pretyping/ functions. | Matthieu Sozeau |
| 2014-09-17 | Fix bug #3593, making constr_eq and progress work up to | Matthieu Sozeau |
| 2014-09-13 | Exporting apply_subfilter from Evd.ml. | Hugo Herbelin |
| 2014-09-13 | Providing a -type-in-type option for collapsing the universe hierarchy. | Hugo Herbelin |
| 2014-09-13 | Checking typability of evar instances. Using ";" to separate bindings | Hugo Herbelin |
| 2014-09-12 | Parsing evar instances. | Hugo Herbelin |
| 2014-09-12 | Referring to evars by names. Added a parser for evars (but parsing of | Hugo Herbelin |
| 2014-08-13 | Bettre pretty-printing of evar maps, avoids printing universe information | Matthieu Sozeau |
| 2014-07-03 | When defining a monomorphic Program, do not allow arbitrary instantiations | Matthieu Sozeau |
| 2014-06-29 | When building on-the-fly elimination principles, set the predicates universe ... | Matthieu Sozeau |
| 2014-06-20 | Cleanup treatment of template universe polymorphism (thanks to E. Tassi | Matthieu Sozeau |
| 2014-06-18 | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau |
| 2014-06-10 | Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un... | Matthieu Sozeau |
| 2014-06-06 | Make kernel reduction code parametric over the handling of universes, | Matthieu Sozeau |
| 2014-06-04 | - Fix hashing of levels to get the "right" order in universe contexts etc... | Matthieu Sozeau |
| 2014-05-08 | - Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ... | Matthieu Sozeau |
| 2014-05-06 | - Fix treatment of global universe constraints which should be passed along | Matthieu Sozeau |
| 2014-05-06 | Find a more efficient fix for dealing with template universes: | Matthieu Sozeau |
| 2014-05-06 | - Fix eq_constr_universes restricted to Sorts.equal | Matthieu Sozeau |
| 2014-05-06 | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau |
| 2014-05-06 | Restore reasonable performance by not allocating during universe checks, | Matthieu Sozeau |
| 2014-05-06 | Correct rebase on STM code. Thanks to E. Tassi for help on dealing with | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-04-23 | Better representation of evar filters: we represent the vacuous filters of | Pierre-Marie Pédrot |
| 2014-03-05 | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey |
| 2014-02-27 | Tacinterp: refactoring using Monad. | Arnaud Spiwack |
| 2014-02-27 | Code refactoring thanks to the new Monad module. | Arnaud Spiwack |
| 2013-11-30 | Useless instantiation function exported in Evd. | Pierre-Marie Pédrot |
| 2013-10-28 | Removing Evd.undefined_evars. | ppedrot |
| 2013-10-27 | Removing useless filter allocation in evar construction. | ppedrot |
| 2013-10-27 | Abstracting evar filter away. The API is not perfect, but better than nothing. | ppedrot |
| 2013-10-22 | Removing useless array-to-list and converse casts used in | ppedrot |
| 2013-10-06 | Removing useless evar code. | ppedrot |
| 2013-10-05 | Removing dubious use of evarmap manipulating functions in printing | ppedrot |
| 2013-10-05 | Moving side effects into evar_map. There was no reason to keep another | ppedrot |
| 2013-09-25 | Removing useless evar-related stuff. | ppedrot |
| 2013-09-18 | At least made the evar type opaque! There are still 5 remaining unsafe | ppedrot |
| 2013-09-05 | Optimizing some evar_maps manipulation. In particular, using a [map] instead | ppedrot |
| 2013-09-05 | Documentation of Evd. | ppedrot |
| 2013-09-03 | Partly replacing list-based access functions in Evd. This is still | ppedrot |
| 2013-08-25 | Added a more efficient way to recover the domain of a map. | ppedrot |
| 2013-08-08 | State Transaction Machine | gareuselesinge |
| 2013-08-04 | Removing now useless merging primitives from Evd. | ppedrot |
| 2013-05-06 | Small cleaning of Evd interface. | ppedrot |
| 2013-05-03 | Removing a redundant function from Evd. | ppedrot |
| 2013-04-29 | Merging Context and Sign. | ppedrot |
| 2013-03-12 | Allowing different types of, not to be mixed, generic Stores through | ppedrot |
