| Commit message (Expand) | Author | Age |
* | Bettre pretty-printing of evar maps, avoids printing universe information | Matthieu Sozeau | 2014-08-13 |
* | When defining a monomorphic Program, do not allow arbitrary instantiations | Matthieu Sozeau | 2014-07-03 |
* | When building on-the-fly elimination principles, set the predicates universe ... | Matthieu Sozeau | 2014-06-29 |
* | 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 |
* | Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un... | Matthieu Sozeau | 2014-06-10 |
* | Make kernel reduction code parametric over the handling of universes, | Matthieu Sozeau | 2014-06-06 |
* | - Fix hashing of levels to get the "right" order in universe contexts etc... | Matthieu Sozeau | 2014-06-04 |
* | - Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ... | Matthieu Sozeau | 2014-05-08 |
* | - 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-05-06 |
* | Better representation of evar filters: we represent the vacuous filters of | Pierre-Marie Pédrot | 2014-04-23 |
* | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey | 2014-03-05 |
* | Tacinterp: refactoring using Monad. | Arnaud Spiwack | 2014-02-27 |
* | Code refactoring thanks to the new Monad module. | Arnaud Spiwack | 2014-02-27 |
* | Useless instantiation function exported in Evd. | Pierre-Marie Pédrot | 2013-11-30 |
* | Removing Evd.undefined_evars. | ppedrot | 2013-10-28 |
* | 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-27 |
* | Removing useless array-to-list and converse casts used in | ppedrot | 2013-10-22 |
* | Removing useless evar code. | ppedrot | 2013-10-06 |
* | 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-10-05 |
* | Removing useless evar-related stuff. | ppedrot | 2013-09-25 |
* | At least made the evar type opaque! There are still 5 remaining unsafe | ppedrot | 2013-09-18 |
* | Optimizing some evar_maps manipulation. In particular, using a [map] instead | ppedrot | 2013-09-05 |
* | Documentation of Evd. | ppedrot | 2013-09-05 |
* | Partly replacing list-based access functions in Evd. This is still | ppedrot | 2013-09-03 |
* | Added a more efficient way to recover the domain of a map. | ppedrot | 2013-08-25 |
* | State Transaction Machine | gareuselesinge | 2013-08-08 |
* | Removing now useless merging primitives from Evd. | ppedrot | 2013-08-04 |
* | Small cleaning of Evd interface. | ppedrot | 2013-05-06 |
* | Removing a redundant function from Evd. | ppedrot | 2013-05-03 |
* | Merging Context and Sign. | ppedrot | 2013-04-29 |
* | Allowing different types of, not to be mixed, generic Stores through | ppedrot | 2013-03-12 |
* | Locating errors from consider_remaining_unif_problems if possible | herbelin | 2013-02-17 |
* | Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_env | herbelin | 2013-01-29 |
* | Modulification of name | ppedrot | 2012-12-18 |
* | Modulification of identifier | ppedrot | 2012-12-14 |
* | Monomorphization (pretyping) | ppedrot | 2012-11-22 |
* | Updating headers. | herbelin | 2012-08-08 |
* | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot | 2012-06-22 |
* | remove many excessive open Util & Errors in mli's | letouzey | 2012-05-29 |
* | Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd | letouzey | 2012-05-29 |
* | Adds a comment: precondition on Evd.add | aspiwack | 2012-04-18 |