aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Univs: bug fix.Gravatar Matthieu Sozeau2015-07-07
* Fix handling of primitive projections in VM.Gravatar Maxime Dénès2015-07-05
* Assumptions: more informative print for False axiom (Close: #4054)Gravatar Enrico Tassi2015-06-29
* Fix incompleteness of conversion used by evarconvGravatar Matthieu Sozeau2015-06-28
* Fix bug #4254 with the help of J.H. JourdanGravatar Matthieu Sozeau2015-06-26
* Make normalization of primitive projections in native_compute the same as wit...Gravatar Maxime Dénès2015-06-08
* Fixup for 866c41bGravatar Enrico Tassi2015-05-28
* Fix bug #4159Gravatar Matthieu Sozeau2015-05-27
* Adding an extensible global state to evarmaps.Gravatar Pierre-Marie Pédrot2015-05-19
* Make Coercion.inh_app_fun respect its specification.Gravatar Pierre-Marie Pédrot2015-05-15
* Disable precompilation for native_compute by default.Gravatar Guillaume Melquiond2015-05-14
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Fix for a second avatar of bug #4234.Gravatar Pierre-Marie Pédrot2015-05-13
* Better fixing #4198 such that the term to match is looked for beforeGravatar Hugo Herbelin2015-05-13
* Fixing bug #4234.Gravatar Pierre-Marie Pédrot2015-05-12
* Code factorization in Constr_matching.Gravatar Pierre-Marie Pédrot2015-05-10
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Tactical `progress` compares term up to potentially equalisable universes.Gravatar Arnaud Spiwack2015-04-22
* Fixing non exhaustive pattern-matching.Gravatar Hugo Herbelin2015-04-22
* Fixing #4198 (looking for subterms also in the return clause of match).Gravatar Hugo Herbelin2015-04-21
* Fixing #3383 (a "return" clause without an "in" clause is not enoughGravatar Hugo Herbelin2015-04-21
* Some dead code.Gravatar Hugo Herbelin2015-04-21
* Really fix constr_of_pattern and bugs #3590 and #4120 byGravatar Matthieu Sozeau2015-04-09
* Remove evars in the type of _unnammed_ metas in pattern_of_constr (fixes Quic...Gravatar Matthieu Sozeau2015-04-09
* Ensuring more invariants in Constr_matching.Gravatar Pierre-Marie Pédrot2015-03-29
* Fixing bug #4165.Gravatar Pierre-Marie Pédrot2015-03-29
* use a more compact representation of non-constant constructorsGravatar Benjamin Gregoire2015-03-27
* Fix bug 4157,Gravatar Benjamin Gregoire2015-03-26
* Fully fixing bug #3491 (anomaly when building _rect scheme in theGravatar Hugo Herbelin2015-03-25
* Use kernel names instead of user names when looking for coercions. (Fix for b...Gravatar Guillaume Melquiond2015-03-25
* Fixing equality of notation_constrs. Fixes bug #4136.Gravatar Pierre-Marie Pédrot2015-03-24
* Add function to fix the non-substituted universe variables of an evar_map.Gravatar Matthieu Sozeau2015-03-17
* Fix bug #3532, providing universe inconsistency information when aGravatar Matthieu Sozeau2015-03-04
* Fix bug #3590, keeping evars that are not turned into named metas byGravatar Matthieu Sozeau2015-03-03
* Fix bug #4103: forgot to allow unfolding projections of cofixpoints likeGravatar Matthieu Sozeau2015-03-03
* Fix bug #4101, noccur_evar's expand_projection can legitimately failGravatar Matthieu Sozeau2015-03-03
* Fix bug introduced by my last commit, forgetting to adjust de BruijnGravatar Matthieu Sozeau2015-03-03
* Fix bug #4097.Gravatar Matthieu Sozeau2015-03-02
* Taking current env and not global env in b286c9f4f42f (4 commits ago,Gravatar Hugo Herbelin2015-02-27
* simpl: honor Global for "simpl: never" (Close: 3206)Gravatar Enrico Tassi2015-02-27
* Add support so that the type of a match in an inductive type with let-inGravatar Hugo Herbelin2015-02-27
* Fixing first part of bug #3210 (inference of pattern-matching returnGravatar Hugo Herbelin2015-02-27
* Fixing typo resulting in wrong printing of return clauses forGravatar Hugo Herbelin2015-02-27
* STM: proof state also includes meta countersGravatar Enrico Tassi2015-02-25
* Still continuing cf6a68b45, d64b5766a and 2734891ab7e on integratingGravatar Hugo Herbelin2015-02-25
* Optimizing noccur_evar wrt expansion of let-ins (fix for variant of #4076).Gravatar Hugo Herbelin2015-02-25
* An optimization on filtering evar instances with let-ins suggested byGravatar Hugo Herbelin2015-02-25
* [Proofview.tclPROGRESS]: do not consider that trivial goal instantiation is p...Gravatar Arnaud Spiwack2015-02-24
* Another bug (de Bruijn) in continuing cf6a68b45 and d64b5766a onGravatar Hugo Herbelin2015-02-24
* Compensating 6fd763431 on postponing subtyping evar-evar problems.Gravatar Hugo Herbelin2015-02-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-14 11:39:11 +0000