From 5ad020d08074993ea6e676e45b4e68491e53e9ed Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 24 May 2009 18:05:50 +0000
Subject: 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
---
 pretyping/evd.ml         | 4 ++--
 pretyping/unification.ml | 6 +++---
 2 files changed, 5 insertions(+), 5 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
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 48c8d65847..f412f54863 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -633,7 +633,7 @@ let w_merge env with_types flags (evd,metas,evars) =
 	      (w_coerce env evd mv c,([],[])),eqns
 	    else
               (* No coercion needed: delay the unification of types *)
-	      ((evd,c),([],[])),(mv,status,c)::eqns
+	      ((evd,c),([],[])),eqns@[(mv,status,c)]
 	  else 
 	    ((evd,c),([],[])),eqns in
 	  if meta_defined evd mv then
@@ -692,8 +692,8 @@ let check_types env flags (sigma,ms,es as subst) m n =
     isEvar_or_Meta (fst (whd_stack sigma n)) then
     let sigma, mt = get_type_of_with_variables env sigma m in
     let sigma, nt = get_type_of_with_variables env sigma n in
-      unify_0_with_initial_metas (sigma,ms,es) true env topconv
-	flags mt nt
+      unify_0_with_initial_metas (sigma,ms,es) true env topconv flags
+	(nf_betaiota sigma mt) (nf_betaiota sigma nt)
   else subst
     
 let w_unify_core_0 env with_types cv_pb flags m n evd =
-- 
cgit v1.2.3