| Commit message (Expand) | Author | Age |
* | Continuing experimentation on what part of the instance of an evar | Hugo Herbelin | 2015-02-21 |
* | Removing dead code. | Pierre-Marie Pédrot | 2015-02-02 |
* | Univs: proper printing of global and local universe names (only | Matthieu Sozeau | 2015-01-17 |
* | Update headers. | Maxime Dénès | 2015-01-12 |
* | New approach to deal with evar-evar unification problems in different | Hugo Herbelin | 2014-12-04 |
* | Option -type-in-type continued (deactivate test for inferred sort of | Hugo Herbelin | 2014-11-19 |
* | new: Optimize Proof, Optimize Heap | Enrico Tassi | 2014-11-09 |
* | Experimentally applying eager evar substitution at the same time as | Hugo Herbelin | 2014-11-04 |
* | Removing dead code from Evd. | Pierre-Marie Pédrot | 2014-10-27 |
* | Removing the Evd.diff function. | Pierre-Marie Pédrot | 2014-10-27 |
* | Removing the Evd.merge function. | Pierre-Marie Pédrot | 2014-10-27 |
* | This commit introduces changes in induction and destruct. | Hugo Herbelin | 2014-10-25 |
* | Refine: proper scoping of the future goals. | Arnaud Spiwack | 2014-10-16 |
* | Move the handling of the principal evar from refine to evd. | Arnaud Spiwack | 2014-10-16 |
* | Move the handling a new evars from the [Proofview.Refine] module to [Evd]. | Arnaud Spiwack | 2014-10-16 |
* | Adding a tactic which fails if one of the goals under focus is dependent in a... | Hugo Herbelin | 2014-10-13 |
* | Add syntax for naming new goals in refine: writing ?[id] instead of _ | Hugo Herbelin | 2014-09-30 |
* | Merging some functions from evarutil.ml/evd.ml. | Hugo Herbelin | 2014-09-29 |
* | Rename eq_constr functions in Evd to not break backward compatibility | Matthieu Sozeau | 2014-09-24 |
* | 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-17 |
* | 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-13 |
* | Parsing evar instances. | Hugo Herbelin | 2014-09-12 |
* | Referring to evars by names. Added a parser for evars (but parsing of | Hugo Herbelin | 2014-09-12 |
* | 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 |