diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-09-15 10:16:56 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-09-15 10:16:56 +0000 |
| commit | 05a07b454b7b1d99950178e19ad2feaa12c44991 (patch) | |
| tree | 0779dcc0c1424f6daf00046d636a2f81902e14b1 /CHANGES | |
| parent | 616e576fd2e79e25464d61f4a9a78eabf5e2edef (diff) | |
MAJ
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9142 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 5 |
1 files changed, 5 insertions, 0 deletions
@@ -3,8 +3,13 @@ Changes from V8.1beta to V8.1 - Support for Miller-Pfenning's patterns unification in type synthesis (e.g. can infer P such that P x y = phi(x,y)) +- Support for Miller-Pfenning's patterns unification in apply/rewrite/... + (may lead to few incompatibilities - generally now useless tactic calls) - Support for implicit arguments in the types of parameters in (co-)fixpoints and (co-)inductive declarations +- Improved type inference: use as much of possible general information + before applying irreversible unification heuristics (allow e.g. to + infer the predicate in "(exist _ 0 (refl_equal 0) : {n:nat | n=0 })") - Support for "where" clause in cofixpoint definitions Changes from V8.0 to V8.1beta |