From 05a07b454b7b1d99950178e19ad2feaa12c44991 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 15 Sep 2006 10:16:56 +0000 Subject: MAJ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9142 85f007b7-540e-0410-9357-904b9bb8a0f7 --- CHANGES | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'CHANGES') diff --git a/CHANGES b/CHANGES index a8494e47a..4b7c42791 100644 --- a/CHANGES +++ b/CHANGES @@ -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 -- cgit v1.2.3