aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Add toplevel commands to declare global universes and constraints.Gravatar Matthieu Sozeau2014-07-01
* Clarifying 'No such bound variable' message in apply, as suggested in #2387Gravatar Hugo Herbelin2014-06-30
* When building on-the-fly elimination principles, set the predicates universe ...Gravatar Matthieu Sozeau2014-06-29
* Really honor the [simpl never] flag in whd_simpl, it was still doing reductio...Gravatar Matthieu Sozeau2014-06-29
* Quick fix of bug #2996 continued (case of inductive types).Gravatar Hugo Herbelin2014-06-28
* Quickly fixing bug #2996: typing functions now check when referring toGravatar Hugo Herbelin2014-06-28
* Moved code for finding subterms (pattern, induction, set, generalize, ...)Gravatar Hugo Herbelin2014-06-28
* Extra check for indirect dependency when abstracting a term which isGravatar Hugo Herbelin2014-06-28
* Made the subterm finding function make_abstraction independent of theGravatar Hugo Herbelin2014-06-28
* Small short optimization of instantiation in Evd.Gravatar Hugo Herbelin2014-06-28
* Fast path in Canonical structure detection. We do not always compute the normalGravatar Pierre-Marie Pédrot2014-06-27
* Deactivate the "Standard Propositions Naming" flag, source of a lot ofGravatar Hugo Herbelin2014-06-26
* Add an option to disable typeclass resolution during conversion, whichGravatar Matthieu Sozeau2014-06-26
* Change interface of refresh universes to get a pbty argument instead ofGravatar Matthieu Sozeau2014-06-26
* Use the right transparent state when comparing _types_ of metas.Gravatar Matthieu Sozeau2014-06-25
* Fix type_of_inductive_knowing_conclusion, relying on an actually broken univ_...Gravatar Matthieu Sozeau2014-06-25
* Use full transparent state when checking well-typedness of a second order mat...Gravatar Matthieu Sozeau2014-06-25
* Fix program cases and inversion tactic to correctly record universe constraints.Gravatar Matthieu Sozeau2014-06-24
* Fix for bug 1951, allowing at least fully-applied inductives types to be usedGravatar Matthieu Sozeau2014-06-23
* - Add an option to refresh only algebraic universes, for e_type_of. The goalGravatar Matthieu Sozeau2014-06-21
* Fixed some HoTT bugs, provide a proper error message when giving an ill-formedGravatar Matthieu Sozeau2014-06-20
* Cleanup treatment of template universe polymorphism (thanks to E. TassiGravatar Matthieu Sozeau2014-06-20
* - Fix bug in unification, not only named metas are turned into evars (e.g. in...Gravatar Matthieu Sozeau2014-06-19
* Proofs now take and return an evar_universe_context, simplifying interfacesGravatar Matthieu Sozeau2014-06-18
* Code factorization in LMap.Gravatar Pierre-Marie Pédrot2014-06-18
* Reinstate eta for records in evarconv, fixing two HoTT coq bugs.Gravatar Matthieu Sozeau2014-06-17
* Adapt coercion code to work with projections as target classes.Gravatar Matthieu Sozeau2014-06-17
* Fixing #3282 (two bugs in the presence of let-in's in "fix").Gravatar Hugo Herbelin2014-06-17
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* Fix type inference of the record argument of a projection to catch ill-typedGravatar Matthieu Sozeau2014-06-17
* - Fix the de Bruijn problem in check_projection for good :)Gravatar Matthieu Sozeau2014-06-17
* Existing Class now works with universe polymorphism. Fixes HoTT bug #063Gravatar Matthieu Sozeau2014-06-17
* Unification in HoTT_coq_061.v was looping with previous commit (whileGravatar Hugo Herbelin2014-06-16
* Fixing part of HoTT bug #61 (in declare_evar_from_virtual_equation,Gravatar Hugo Herbelin2014-06-16
* - Add "Show Universes" to print information about universes during a proof.Gravatar Matthieu Sozeau2014-06-16
* Change Ltac constr matching semantics to consider universes when merging twoGravatar Matthieu Sozeau2014-06-15
* Fix HoTT/coq bug # 14. Now coercion code correctly raises an error instead of...Gravatar Matthieu Sozeau2014-06-13
* Fixing "clear" in internal_cut_replace: forbid dependencies in theGravatar Hugo Herbelin2014-06-13
* Improved error message when a meta posed as an evar remains unsolvedGravatar Hugo Herbelin2014-06-13
* Fixing wrong environment for Meta's in pose_all_metas_as_evars (bug #3284).Gravatar Hugo Herbelin2014-06-13
* Adapt simpl/cbn unfolding and refolding machinery to projections, so thatGravatar Matthieu Sozeau2014-06-13
* - Fix bug #3368, due to wrong use of the Cst_stack for projections.Gravatar Matthieu Sozeau2014-06-11
* In generalized rewrite, avoid retyping completely and constantly the conclusi...Gravatar Matthieu Sozeau2014-06-11
* Compute the trace of a universe inconsistency only when explicitly requiredGravatar Pierre-Marie Pédrot2014-06-10
* Made explanations for universe inconsistencies optional. They are only usedGravatar Pierre-Marie Pédrot2014-06-10
* - Fix substitution of universes which needlessly hashconsed existing universes.Gravatar Matthieu Sozeau2014-06-10
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Gravatar Matthieu Sozeau2014-06-10
* Fix canonical structure resolution in unification (bug found in Ssreflect).Gravatar Matthieu Sozeau2014-06-08
* Make kernel reduction code parametric over the handling of universes,Gravatar Matthieu Sozeau2014-06-06
* Collecting in Namegen those conventional default names that are used in diffe...Gravatar Hugo Herbelin2014-06-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 08:43:54 +0000