| Age | Commit message (Expand) | Author |
|---|
| 2014-10-25 | This commit introduces changes in induction and destruct. | Hugo Herbelin |
| 2014-10-22 | Add more primitives to the [Monad.Make] arguments. | Arnaud Spiwack |
| 2014-10-21 | Dead code. | Hugo Herbelin |
| 2014-10-16 | 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 | Evd: a few comments to document the increasingly wide internal [evar_map] type. | Arnaud Spiwack |
| 2014-10-16 | Evd: remove/update obsolete comments. | Arnaud Spiwack |
| 2014-10-13 | Adding a tactic which fails if one of the goals under focus is dependent in a... | Hugo Herbelin |
| 2014-10-10 | Add debug printers for projections, fix printing of evar constraints | Matthieu Sozeau |
| 2014-10-03 | Fixing ennoying warning about evars named ?23 and so on. | Hugo Herbelin |
| 2014-10-02 | Work around issues with FO unification trying to unify terms of | Matthieu Sozeau |
| 2014-09-30 | Seeing IntroWildcard as an action intro pattern rather than as a naming pattern | Hugo Herbelin |
| 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 | Fixing synchronization of evar names table when merging evar_map. | 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-08-09 | Using the asymmetric merging primitive in Evd. | Pierre-Marie Pédrot |
| 2014-08-09 | Cleaning up interface of ContextSet. | Pierre-Marie Pédrot |
| 2014-08-09 | Tentative performance fix for Evd.merge_uctx. | Pierre-Marie Pédrot |
| 2014-08-05 | Small code simplification. | Pierre-Marie Pédrot |
| 2014-07-20 | Use kernel conversion on terms that contain universe variables during unifica... | Matthieu Sozeau |
| 2014-07-03 | When defining a monomorphic Program, do not allow arbitrary instantiations | Matthieu Sozeau |
| 2014-06-30 | Clarifying 'No such bound variable' message in apply, as suggested in #2387 | Hugo Herbelin |
| 2014-06-29 | When building on-the-fly elimination principles, set the predicates universe ... | Matthieu Sozeau |
| 2014-06-28 | Small short optimization of instantiation in Evd. | Hugo Herbelin |
| 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-18 | Code factorization in LMap. | Pierre-Marie Pédrot |
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot |
| 2014-06-13 | Improved error message when a meta posed as an evar remains unsolved | Hugo Herbelin |
| 2014-06-10 | Made explanations for universe inconsistencies optional. They are only used | Pierre-Marie Pédrot |
| 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-06 | Make kernel reduction code parametric over the handling of universes, | Matthieu Sozeau |
| 2014-06-04 | - Force every universe level to be >= Prop, so one cannot "go under" it anymore. | Matthieu Sozeau |
| 2014-06-04 | - Fix hashing of levels to get the "right" order in universe contexts etc... | Matthieu Sozeau |
| 2014-06-04 | - Keep all <= constraints during refinement, otherwise we might miss collapse... | Matthieu Sozeau |
| 2014-05-28 | - Fix for commit 15999903f875f4b5dbb3d5240d2ca39acc3cd777 which disallowed some | Matthieu Sozeau |
| 2014-05-26 | - Fix in kernel conversion not folding the universe constraints | 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 |
