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