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
*
Improve return predicate inference by making the return type dependent
msozeau
2009-06-28
*
Fixes for r12197, the refined evars were not returned in case fail_evar
msozeau
2009-06-22
*
documented a bug of pattern unification with metas
barras
2009-06-22
*
Use more consistent resolution parameters in Program and regular typing
msozeau
2009-06-18
*
Fix "unsatisfiable constraints" error messages to include all the
msozeau
2009-06-18
*
Try typeclass resolution in coercion if no solution can be found to a
msozeau
2009-06-18
*
Use a lazy value for the message in FailError, so that it won't be
msozeau
2009-06-11
*
When typing a non-dependent arrow, do not put the (anonymous) variable
msozeau
2009-06-11
*
Fixing bug #2106 ("match" compilation with multi-dependent constructor).
herbelin
2009-06-06
*
Adding a regression test about Bauer's example on coq-club of
herbelin
2009-06-02
*
Backtrack on experimental unification with sort variables: it requires
msozeau
2009-06-02
*
Change unification with sort constraints to not use the kernel
msozeau
2009-06-01
*
Properly catch sort constraint inconsistency exception in
msozeau
2009-05-28
*
Populate the sort constraints set correctly during unification. Add a
msozeau
2009-05-27
*
Temporary fixes in unification:
msozeau
2009-05-24
*
A try at using sort variables during unification. Instead of refreshing
msozeau
2009-05-23
*
Many fixes in unification:
msozeau
2009-05-20
*
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
[next]