Fixes to make Ynot compile with the trunk:

- Choose one of the possible instances of an evar when considering
remaining unification constraints: otherwise we just do nothing and
some evars remain uninstantiated.
- Normalise the goal w.r.t. evars before subst, to avoid a double vision 
problem: the substituted variable appears only in an instance of an evar
and when we try the rewrite it has been substituted making the dependency
disappear.
- Hack to correcly handle let-in annotations which are internalized as 
casts: they're really typing constraints. Shouldn't we just change the 
AST to have the type at rawconstr let-in nodes?


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11998 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions