index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
Commit message (
Expand
)
Author
Age
*
Fixing bug #4303: Anomaly: Uncaught exception Invalid_argument.
Pierre-Marie Pédrot
2015-07-21
*
Refining 71def2f8 on too strong occur-check limiting evar-evar
Hugo Herbelin
2015-07-16
*
Slight improvement in naming anonymous variables in error messages:
Hugo Herbelin
2015-07-16
*
Fixing #4177 (find_projectable was liable to ask to instantiate an evar twice).
Hugo Herbelin
2015-07-16
*
Fixing bug #4240 (closure_of_filter was not ensuring refinement of
Hugo Herbelin
2015-07-16
*
Fix universe instantiation with canonical structures.
Maxime Dénès
2015-07-16
*
Continuing 93579407, spotting other potential sources of anomaly
Hugo Herbelin
2015-07-16
*
Fixing anomaly #3743 while printing an error message involving evar constraints.
Hugo Herbelin
2015-07-16
*
Continuing handling of NoCoercion after df6e64fd28 and 4944b5e72.
Hugo Herbelin
2015-07-10
*
Option -type-in-type: added support in checker and making it contaminating
Hugo Herbelin
2015-07-10
*
Make retyping of projections more resilient to wrong environment.
Maxime Dénès
2015-07-09
*
Univs: bug fix.
Matthieu Sozeau
2015-07-07
*
Fix handling of primitive projections in VM.
Maxime Dénès
2015-07-05
*
Assumptions: more informative print for False axiom (Close: #4054)
Enrico Tassi
2015-06-29
*
Fix incompleteness of conversion used by evarconv
Matthieu Sozeau
2015-06-28
*
Fix bug #4254 with the help of J.H. Jourdan
Matthieu Sozeau
2015-06-26
*
Make normalization of primitive projections in native_compute the same as wit...
Maxime Dénès
2015-06-08
*
Fixup for 866c41b
Enrico Tassi
2015-05-28
*
Fix bug #4159
Matthieu Sozeau
2015-05-27
*
Adding an extensible global state to evarmaps.
Pierre-Marie Pédrot
2015-05-19
*
Make Coercion.inh_app_fun respect its specification.
Pierre-Marie Pédrot
2015-05-15
*
Disable precompilation for native_compute by default.
Guillaume Melquiond
2015-05-14
*
Safer typing primitives.
Pierre-Marie Pédrot
2015-05-13
*
Fix for a second avatar of bug #4234.
Pierre-Marie Pédrot
2015-05-13
*
Better fixing #4198 such that the term to match is looked for before
Hugo Herbelin
2015-05-13
*
Fixing bug #4234.
Pierre-Marie Pédrot
2015-05-12
*
Code factorization in Constr_matching.
Pierre-Marie Pédrot
2015-05-10
*
Remove almost all the uses of string concatenation when building error messages.
Guillaume Melquiond
2015-04-23
*
Tactical `progress` compares term up to potentially equalisable universes.
Arnaud Spiwack
2015-04-22
*
Fixing non exhaustive pattern-matching.
Hugo Herbelin
2015-04-22
*
Fixing #4198 (looking for subterms also in the return clause of match).
Hugo Herbelin
2015-04-21
*
Fixing #3383 (a "return" clause without an "in" clause is not enough
Hugo Herbelin
2015-04-21
*
Some dead code.
Hugo Herbelin
2015-04-21
*
Really fix constr_of_pattern and bugs #3590 and #4120 by
Matthieu Sozeau
2015-04-09
*
Remove evars in the type of _unnammed_ metas in pattern_of_constr (fixes Quic...
Matthieu Sozeau
2015-04-09
*
Ensuring more invariants in Constr_matching.
Pierre-Marie Pédrot
2015-03-29
*
Fixing bug #4165.
Pierre-Marie Pédrot
2015-03-29
*
use a more compact representation of non-constant constructors
Benjamin Gregoire
2015-03-27
*
Fix bug 4157,
Benjamin Gregoire
2015-03-26
*
Fully fixing bug #3491 (anomaly when building _rect scheme in the
Hugo Herbelin
2015-03-25
*
Use kernel names instead of user names when looking for coercions. (Fix for b...
Guillaume Melquiond
2015-03-25
*
Fixing equality of notation_constrs. Fixes bug #4136.
Pierre-Marie Pédrot
2015-03-24
*
Add function to fix the non-substituted universe variables of an evar_map.
Matthieu Sozeau
2015-03-17
*
Fix bug #3532, providing universe inconsistency information when a
Matthieu Sozeau
2015-03-04
*
Fix bug #3590, keeping evars that are not turned into named metas by
Matthieu Sozeau
2015-03-03
*
Fix bug #4103: forgot to allow unfolding projections of cofixpoints like
Matthieu Sozeau
2015-03-03
*
Fix bug #4101, noccur_evar's expand_projection can legitimately fail
Matthieu Sozeau
2015-03-03
*
Fix bug introduced by my last commit, forgetting to adjust de Bruijn
Matthieu Sozeau
2015-03-03
*
Fix bug #4097.
Matthieu Sozeau
2015-03-02
*
Taking current env and not global env in b286c9f4f42f (4 commits ago,
Hugo Herbelin
2015-02-27
[next]