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
*
Fix in canonical structure resolution: [check_conv_record] may return
msozeau
2009-05-19
*
Remove camlp4-specific exception handling
msozeau
2009-05-19
*
Minor unification changes:
msozeau
2009-05-18
*
(Tentative to) add Canonical Structure resolution to the regular
msozeau
2009-05-16
*
- Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: it
herbelin
2009-05-10
*
- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence
herbelin
2009-05-09
*
fix a bug in canonical structures (bug found and fixed by Cyril)
barras
2009-05-09
*
- Implementation of a new typeclasses eauto procedure based on success
msozeau
2009-04-27
*
- Fixing #2090 (occur check missing when trying to solve evar-evar equation).
herbelin
2009-04-25
*
- New cleaning phase for the entry points of pretyping.ml
herbelin
2009-04-24
*
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
[next]