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
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-06-01
|
\
|
*
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
*
|
Merge v8.5 into trunk
Hugo Herbelin
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
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-05-05
|
\
|
|
*
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
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-04-15
|
\
|
|
*
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
*
|
Merge branch 'v8.5' into trunk
Enrico Tassi
2015-03-30
|
\
|
|
*
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
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-03-04
|
\
|
|
*
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
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-02-28
|
\
|
|
*
Taking current env and not global env in b286c9f4f42f (4 commits ago,
Hugo Herbelin
2015-02-27
|
*
simpl: honor Global for "simpl: never" (Close: 3206)
Enrico Tassi
2015-02-27
|
*
Add support so that the type of a match in an inductive type with let-in
Hugo Herbelin
2015-02-27
|
*
Fixing first part of bug #3210 (inference of pattern-matching return
Hugo Herbelin
2015-02-27
|
*
Fixing typo resulting in wrong printing of return clauses for
Hugo Herbelin
2015-02-27
*
|
Adding a new folder corresponding to the low-level part of the pretyper
Pierre-Marie Pédrot
2015-02-27
|
/
*
STM: proof state also includes meta counters
Enrico Tassi
2015-02-25
*
Still continuing cf6a68b45, d64b5766a and 2734891ab7e on integrating
Hugo Herbelin
2015-02-25
*
Optimizing noccur_evar wrt expansion of let-ins (fix for variant of #4076).
Hugo Herbelin
2015-02-25
*
An optimization on filtering evar instances with let-ins suggested by
Hugo Herbelin
2015-02-25
*
[Proofview.tclPROGRESS]: do not consider that trivial goal instantiation is p...
Arnaud Spiwack
2015-02-24
[next]