| Age | Commit message (Expand) | Author |
|---|
| 2014-08-05 | A new step in the new "standard" naming policy for propositional hypotheses | Hugo Herbelin |
| 2014-08-03 | - Fix handling of opaque polymorphic definitions which were turned transparent. | Matthieu Sozeau |
| 2014-08-03 | Move to a representation of universe polymorphic constants using indices for ... | Matthieu Sozeau |
| 2014-08-03 | - Fix has_undefined_evars not using its or_sorts argument anymore. | Matthieu Sozeau |
| 2014-08-01 | Continuing (incomplete) cleaning of Inductiveops. | Hugo Herbelin |
| 2014-08-01 | A tentative uniform naming policy in module Inductiveops. | Hugo Herbelin |
| 2014-07-31 | Add an option to solve typeclass goals generated by apply which can't be | Matthieu Sozeau |
| 2014-07-30 | Avoid introducing additional universes when doing pruning in evarsolve. | Matthieu Sozeau |
| 2014-07-29 | Rework code for refolding projections in whd_state/whd_simpl to allow Arguments | Matthieu Sozeau |
| 2014-07-29 | Fix bug #3453, not recognizing primitive projections in Coercion declarations. | Matthieu Sozeau |
| 2014-07-20 | Use kernel conversion on terms that contain universe variables during unifica... | Matthieu Sozeau |
| 2014-07-17 | Fix coercion code to disallow using cumulativity in the domain of products, w... | Matthieu Sozeau |
| 2014-07-14 | Add interface function to replace new_Type () | Matthieu Sozeau |
| 2014-07-10 | Reduce non-toplevel letins in splay_prod_assum (bug found in Ergo). | Matthieu Sozeau |
| 2014-07-09 | Revert patch making the oracle be used for the transparent state in evarconv, | Matthieu Sozeau |
| 2014-07-07 | In flex-flex cases, the undefinedness of an evar can not be preseved after co... | Matthieu Sozeau |
| 2014-07-07 | Missing check of evar instantiation, resulting in missing constraints (bug fr... | Matthieu Sozeau |
| 2014-07-03 | Cleanup code related to the constraint solving, which sits now outside the | Matthieu Sozeau |
| 2014-07-03 | Fix eta expansion of primitive records (HoTT bug #78), which now fails cleanl... | Matthieu Sozeau |
| 2014-07-03 | When defining a monomorphic Program, do not allow arbitrary instantiations | Matthieu Sozeau |
| 2014-07-02 | Fix a Not_found anomaly raised by solve_evar_evar, we were breaking the | Matthieu Sozeau |
| 2014-07-01 | Add toplevel commands to declare global universes and constraints. | 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-29 | Really honor the [simpl never] flag in whd_simpl, it was still doing reductio... | Matthieu Sozeau |
| 2014-06-28 | Quick fix of bug #2996 continued (case of inductive types). | Hugo Herbelin |
| 2014-06-28 | Quickly fixing bug #2996: typing functions now check when referring to | Hugo Herbelin |
| 2014-06-28 | Moved code for finding subterms (pattern, induction, set, generalize, ...) | Hugo Herbelin |
| 2014-06-28 | Extra check for indirect dependency when abstracting a term which is | Hugo Herbelin |
| 2014-06-28 | Made the subterm finding function make_abstraction independent of the | Hugo Herbelin |
| 2014-06-28 | Small short optimization of instantiation in Evd. | Hugo Herbelin |
| 2014-06-27 | Fast path in Canonical structure detection. We do not always compute the normal | Pierre-Marie Pédrot |
| 2014-06-26 | Deactivate the "Standard Propositions Naming" flag, source of a lot of | Hugo Herbelin |
| 2014-06-26 | Add an option to disable typeclass resolution during conversion, which | Matthieu Sozeau |
| 2014-06-26 | Change interface of refresh universes to get a pbty argument instead of | Matthieu Sozeau |
| 2014-06-25 | Use the right transparent state when comparing _types_ of metas. | Matthieu Sozeau |
| 2014-06-25 | Fix type_of_inductive_knowing_conclusion, relying on an actually broken univ_... | Matthieu Sozeau |
| 2014-06-25 | Use full transparent state when checking well-typedness of a second order mat... | Matthieu Sozeau |
| 2014-06-24 | Fix program cases and inversion tactic to correctly record universe constraints. | Matthieu Sozeau |
| 2014-06-23 | Fix for bug 1951, allowing at least fully-applied inductives types to be used | Matthieu Sozeau |
| 2014-06-21 | - Add an option to refresh only algebraic universes, for e_type_of. The goal | Matthieu Sozeau |
| 2014-06-20 | Fixed some HoTT bugs, provide a proper error message when giving an ill-formed | Matthieu Sozeau |
| 2014-06-20 | Cleanup treatment of template universe polymorphism (thanks to E. Tassi | Matthieu Sozeau |
| 2014-06-19 | - Fix bug in unification, not only named metas are turned into evars (e.g. in... | 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 | Reinstate eta for records in evarconv, fixing two HoTT coq bugs. | Matthieu Sozeau |
| 2014-06-17 | Adapt coercion code to work with projections as target classes. | Matthieu Sozeau |
| 2014-06-17 | Fixing #3282 (two bugs in the presence of let-in's in "fix"). | Hugo Herbelin |
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot |
