Temporary fixes in unification:

- Solve meta type equations in the order they appeared during
  unification: it's sensible because we do an [hnf_constr] on these
  types, introducing a bit of delta even when it's not allowed by the
  flags, and some code relies on it. A definite solution would involve an
  nf variant of hnf_constr or allowing delta-reduction of closed terms 
  when unifying types.
- Do a bit of betaiota reduction on types in [check_types] while we
  haven't got a sort-variable aware [is_trans_fconv] test.


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

0 files changed, 0 insertions, 0 deletions