More robust and uniform treatment of aliases in evarutil.ml

- Compute chain of aliases once for all so as to simplify code.
- In is_unification_pattern, expand all vars/rels of the unification
  problem until they are no longer vars/rels so that the list of
  vars/rels used in the rhs is correct, and, the list of arguments of
  the evars eventually become irreducible vars/rels (in particular,
  this solves bug #2615).
- Some points remain unclear, e.g. whether solve_evar_evar should
  reason with all let-in expanded or with let-in expanded only up
  to the last expansion which is still a var or rel.

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

0 files changed, 0 insertions, 0 deletions