aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Use kernel conversion on terms that contain universe variables during unifica...Gravatar Matthieu Sozeau2014-07-20
* Fix coercion code to disallow using cumulativity in the domain of products, w...Gravatar Matthieu Sozeau2014-07-17
* Add interface function to replace new_Type ()Gravatar Matthieu Sozeau2014-07-14
* Reduce non-toplevel letins in splay_prod_assum (bug found in Ergo).Gravatar Matthieu Sozeau2014-07-10
* Revert patch making the oracle be used for the transparent state in evarconv,Gravatar Matthieu Sozeau2014-07-09
* In flex-flex cases, the undefinedness of an evar can not be preseved after co...Gravatar Matthieu Sozeau2014-07-07
* Missing check of evar instantiation, resulting in missing constraints (bug fr...Gravatar Matthieu Sozeau2014-07-07
* Cleanup code related to the constraint solving, which sits now outside theGravatar Matthieu Sozeau2014-07-03
* Fix eta expansion of primitive records (HoTT bug #78), which now fails cleanl...Gravatar Matthieu Sozeau2014-07-03
* When defining a monomorphic Program, do not allow arbitrary instantiationsGravatar Matthieu Sozeau2014-07-03
* Fix a Not_found anomaly raised by solve_evar_evar, we were breaking theGravatar Matthieu Sozeau2014-07-02
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 12:35:39 +0000