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
*
fixed CBV strategy: it was too eager on terms like
barras
2009-04-21
*
- Fix handling of clauses in setoid_rewrite to rewrite under binders
msozeau
2009-04-17
*
Fix premature optimisation in dependent induction: even variable args need
msozeau
2009-04-10
*
Backtrack on 12061 (type checking for bug #2084 too strong as soon as we use
herbelin
2009-04-09
*
Some dead code removal + cleanups
letouzey
2009-04-08
*
- Fixing bug #2084 (unification not checking sort constraints), hoping
herbelin
2009-04-08
*
- Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixing
herbelin
2009-04-08
*
Fix obvious bug in evars_of_named_context.
msozeau
2009-04-03
*
Rewrite of Program Fixpoint to overcome the previous limitations:
msozeau
2009-03-28
*
Fix bug #2056 (discharge bug).
msozeau
2009-03-28
*
Compromise wrt introduction-names compatibility issue after addition
herbelin
2009-03-22
*
Many changes in the Makefile infrastructure + a beginning of ocamlbuild
letouzey
2009-03-20
*
Fixes to make Ynot compile with the trunk:
msozeau
2009-03-20
*
Backtrack sur la mémoïsation de nf_evar.
aspiwack
2009-03-04
*
=?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=...
aspiwack
2009-02-27
*
On passe les last_mods (un des champs de Evd.evar_defs) de list
aspiwack
2009-02-20
*
On ne met plus rien dans les last_mods tant que conv_pbs est vide.
aspiwack
2009-02-20
*
On remplace evar_map par evar_defs (seul evar_defs est désormais exporté
aspiwack
2009-02-19
*
memoized is_ground_env
barras
2009-02-09
*
pushed evar reduction in kernel
barras
2009-02-06
*
From v8.2 to trunk:
herbelin
2009-02-06
*
Really compare evar maps in progress, due to merging in apply and other
msozeau
2009-01-23
*
Fixing bug #1918 (no occur-check in Meta unification was done yet!).
herbelin
2009-01-20
*
- Fixing bug 1891 (abusive instantiations of evar arguments in
herbelin
2009-01-20
*
Backporting from v8.2 to trunk:
herbelin
2009-01-18
*
DISCLAIMER
puech
2009-01-17
*
Correct a bug in commit 11659
puech
2009-01-16
*
Fix a bunch of bugs related to setoid_rewrite, unification and evars:
msozeau
2009-01-12
*
Completed 11745 (move of jprover to user contribs) and cleaned 11743
herbelin
2009-01-05
*
Fixed bugs #2001 (search_guard was overwriting the guard index given
herbelin
2009-01-04
*
Fixed two apparent inconsistencies in matching.ml:
herbelin
2009-01-02
*
Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->
herbelin
2008-12-31
*
- Added support for subterm matching in SearchAbout.
herbelin
2008-12-29
*
- Another bug in get_sort_family_of (sort-polymorphism of constants and
herbelin
2008-12-28
*
- Extracted from the tactic "now" an experimental tactic "easy" for small
herbelin
2008-12-26
*
Fix exponential behaviour of the typeclasses persistent objects. Drop
puech
2008-12-06
*
Fixes for unification and substitution of metas under binders.
msozeau
2008-12-04
*
improved simpl
barras
2008-12-03
*
Miscellaneous fixes and improvements:
herbelin
2008-12-02
*
another bug with simpl
barras
2008-11-28
*
Fix (?) a pattern matching compilation problem:
msozeau
2008-11-27
*
fixed bug 1791: simpl was performing eta expansion
barras
2008-11-27
*
fixing problem with CompCert: reordering resulting from tac change was not cl...
barras
2008-11-27
*
fixed problem with r11612
barras
2008-11-21
*
fixed exponential behavior of evar unif (ground case)
barras
2008-11-21
*
Restores behaviour of v8.1 for unification problems which fail (backport of 1...
letouzey
2008-11-14
*
- Fixed bug 1968 (inversion failing due to a Not_found bug introduced in
herbelin
2008-11-09
*
Apply vmconv if there are no _undefined_ evars around.
msozeau
2008-11-08
*
Slight change of the semantics of user-given casts: they don't really
msozeau
2008-11-07
*
Fix universe problem appearing ConCaT using the existing infrastructure for
msozeau
2008-11-07
[next]