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

1 files changed, 2 insertions, 2 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 79cdc7da58..cfdd76de8b 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -610,11 +610,11 @@ let universes_to_variables_gen strict evd t =
   let evdref = ref evd in
   let rec refresh t = match kind_of_term t with
     | Sort (Type u as us) when strict or u <> Univ.type0m_univ ->
-(* 	if Univ.is_univ_variable u then  *)
+	if not (is_sort_variable !evdref us) then
 	  let s', evd = new_sort_variable !evdref in
 	  let evd = set_leq_sort_variable evd s' us in
 	    evdref := evd; modified := true; mkSort s'
-(* 	else t *)
+	else t
     | Prod (na,u,v) -> mkProd (na,u,refresh v)
     | _ -> t in
   let t' = refresh t in