Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Continuation of r16346 on filtering local definitions. Refined | 2013-03-30 | |
| | | | | | | | | | | | | the "choose less dependent" constraint-solving heuristic so that it is not disturbed by local definitions. This is a quick fix. A deeper analysis of the structure of constraints of the form ?x[args] = y, determining if variable y can itself be a local def or not, and whether args can be let-ins aliasing other variables, would allow to know if the fix needs to be refined further. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16376 85f007b7-540e-0410-9357-904b9bb8a0f7 | ||
* | Evarconv: When doing a iota of a fixpoint, use constant name instead of ↵ | 2013-02-25 | |
| | | | | | | | | fixpoint definition + Help the use of #trace on evar_conv_appr_x git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16244 85f007b7-540e-0410-9357-904b9bb8a0f7 | ||
* | A small test for type inference (used to be a regression at some time). | 2011-12-04 | |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14759 85f007b7-540e-0410-9357-904b9bb8a0f7 |