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
*
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
*
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
*
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
*
Another bug (de Bruijn) in continuing cf6a68b45 and d64b5766a on
Hugo Herbelin
2015-02-24
*
Compensating 6fd763431 on postponing subtyping evar-evar problems.
Hugo Herbelin
2015-02-23
*
Fixing cf6a68b45 on integrating ensure_evar_independent into is_constrainable...
Hugo Herbelin
2015-02-23
*
Fix some typos in comments.
Guillaume Melquiond
2015-02-23
*
Fixing rewrite/subst when the subterm to rewrite is argument of an Evar.
Hugo Herbelin
2015-02-23
*
Fixing occur-check which was too strong in unification.ml.
Hugo Herbelin
2015-02-23
*
Fixing bug #3071.
Pierre-Marie Pédrot
2015-02-21
*
Continuing experimentation on what part of the instance of an evar
Hugo Herbelin
2015-02-21
*
Removing need for ensure_evar_independent by passing a force flag to is_const...
Hugo Herbelin
2015-02-21
*
When looking for restrictions in ?n=?p problems, keep the type of let-bindings.
Hugo Herbelin
2015-02-19
*
Remove some dead code and add test-suite file.
Matthieu Sozeau
2015-02-16
*
Fix bug #3960: potential evar instance categorized as an unresolvable
Matthieu Sozeau
2015-02-16
*
Fix 'don't expose cases' in cbn
Pierre Boutillier
2015-02-15
*
Fixing bug #3490.
Pierre-Marie Pédrot
2015-02-15
*
Fixing bug #3916.
Pierre-Marie Pédrot
2015-02-15
*
Univs: fix bug #3755. We were missing refreshements of universes in
Matthieu Sozeau
2015-02-14
*
Fixing #3997 (occur-check in the presence of primitive projections, patch
Hugo Herbelin
2015-02-12
[next]