Backtrack on experimental unification with sort variables: it requires

major changes in [w_unify] and the conversion functions used by it to
handle the sort constraints correctly.


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

7 files changed, 84 insertions, 212 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 695d93ca89..dd2af306c9 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -73,8 +73,7 @@ let clenv_push_prod cl =
 	let mv = new_meta () in
 	let dep = dependent (mkRel 1) u in
 	let na' = if dep then na else Anonymous in
-	let evd,t' = Evd.universes_to_variables cl.evd t in
-	let e' = meta_declare mv t' ~name:na' evd in
+	let e' = meta_declare mv t ~name:na' cl.evd in
 	let concl = if dep then subst1 (mkMeta mv) u else u in
 	let def = applist (cl.templval.rebus,[mkMeta mv]) in
 	{ templval = mk_freelisted def;
@@ -96,8 +95,7 @@ let clenv_environments evd bound t =
 	  let mv = new_meta () in
 	  let dep = dependent (mkRel 1) t2 in
 	  let na' = if dep then na else Anonymous in
-	  let e',t1' = Evd.universes_to_variables e t1 in
-	  let e' = meta_declare mv t1' ~name:na' e' in
+	  let e' = meta_declare mv t1 ~name:na' e in
 	  clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n)
 	    (if dep then (subst1 (mkMeta mv) t2) else t2)
       | (n, LetIn (na,b,_,t)) -> clrec (e,metas) n (subst1 b t)
@@ -114,8 +112,7 @@ let clenv_environments_evars env evd bound t =
       | (Some 0, _) -> (e, List.rev ts, t)
       | (n, Cast (t,_,_)) -> clrec (e,ts) n t
       | (n, Prod (na,t1,t2)) ->
-	  let e',t1' = Evd.universes_to_variables e t1 in
-          let e',constr = Evarutil.new_evar e' env t1' in
+          let e',constr = Evarutil.new_evar e env t1 in
 	  let dep = dependent (mkRel 1) t2 in
 	  clrec (e', constr::ts) (Option.map ((+) (-1)) n)
 	    (if dep then (subst1 constr t2) else t2)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index a7c978168f..d6b10b7d0e 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -24,40 +24,6 @@ open Evarutil
 open Libnames
 open Evd
 
-let base_sort_conv evd pb s1 s2 =
-  try
-    match (s1,s2) with
-    | (Prop c1, Prop c2) -> if c1 = Null or c2 = Pos then Some evd else None (* Prop <= Set *)
-    | (Prop c1, Type u)  -> 
-	if pb = Reduction.CUMUL then Some evd 
-	else if Evd.is_sort_variable evd s2 then
-	  Some (Evd.define_sort_variable evd s2 s1)
-	else None
-    | (Type u, Prop c)   -> 
-	if Evd.is_sort_variable evd s1 then
-	  Some (Evd.define_sort_variable evd s1 s2)
-	else None
-    | (Type u1, Type u2) -> 
-	match pb with
-	| CONV -> Some (Evd.set_eq_sort_variable evd s1 s2)
-	| CUMUL -> Some (Evd.set_leq_sort_variable evd s1 s2)
-  with e -> None
-
-let unify_constr_univ evd f cv_pb t1 t2 = 
-  match kind_of_term t1, kind_of_term t2 with
-      Sort s1, Sort s2 -> 
-	(match base_sort_conv !evd cv_pb s1 s2 with
-	| Some evd' -> evd := evd'; true
-	| None -> false)
-    | Prod (_,t1,c1), Prod (_,t2,c2) -> 
-	f Reduction.CONV t1 t2 & f cv_pb c1 c2
-    | _ -> compare_constr (f Reduction.CONV) t1 t2
-
-let constr_unify_with_sorts evd cv_pb t1 t2 = 
-  let evdref = ref evd in
-  let rec aux cv_pb t1 t2 = unify_constr_univ evdref aux cv_pb t1 t2 in
-    if aux cv_pb t1 t2 then true, !evdref else false, evd
-
 type flex_kind_of_term =
   | Rigid of constr 
   | MaybeFlexible of constr
@@ -410,10 +376,8 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	| _, Cast (c2,_,_) -> evar_eqappr_x env evd pbty appr1 (c2,l2)
 
 	| Sort s1, Sort s2 when l1=[] & l2=[] ->
-	    (match base_sort_conv evd pbty s1 s2 with
-	    | Some evd' -> evd',true
-	    | None -> evd, false)
-	      
+            (evd,base_sort_cmp pbty s1 s2)
+
 	| Lambda (na,c1,c'1), Lambda (_,c2,c'2) when l1=[] & l2=[] -> 
             ise_and evd
               [(fun i -> evar_conv_x env i CONV c1 c2);
@@ -578,11 +542,11 @@ let apply_conversion_problem_heuristic env evd pbty t1 t2 =
 
 let consider_remaining_unif_problems env evd =
   let (evd,pbs) = extract_all_conv_pbs evd in
-    List.fold_left
-      (fun (evd,b as p) (pbty,env,t1,t2) ->
-	if b then apply_conversion_problem_heuristic env evd pbty t1 t2 else p)
-      (evd,true)
-      pbs
+  List.fold_left
+    (fun (evd,b as p) (pbty,env,t1,t2) ->
+      if b then apply_conversion_problem_heuristic env evd pbty t1 t2 else p)
+    (evd,true)
+    pbs
 
 (* Main entry points *)
 
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index ec42476003..a281a3898f 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -16,13 +16,6 @@ open Reductionops
 open Evd
 (*i*)
 
-(* Comparison function considering sort variables. *)
-val base_sort_conv : evar_defs -> conv_pb ->
-  sorts -> sorts -> evar_defs option
-
-val constr_unify_with_sorts : evar_defs -> conv_pb ->
-  types -> types -> bool * evar_defs
-
 (* returns exception Reduction.NotConvertible if not unifiable *)
 val the_conv_x     : env -> constr -> constr -> evar_defs -> evar_defs
 val the_conv_x_leq : env -> constr -> constr -> evar_defs -> evar_defs
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index ecad02cd40..191c8e62af 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -184,25 +184,21 @@ type sort_constraints = sort_constraint UniverseMap.t
 
 let rec canonical_find u scstr =
   match UniverseMap.find u scstr with
-  | EqSort u' -> canonical_find u' scstr
-  | c -> (u,c)
-
-let find_univ u scstr =
-  try canonical_find u scstr
-  with Not_found -> u, DefinedSort (Type u)
+      EqSort u' -> canonical_find u' scstr
+    | c -> (u,c)
 
 let whd_sort_var scstr t =
   match kind_of_term t with
       Sort(Type u) ->
         (try
           match canonical_find u scstr with
-          | _, DefinedSort s -> mkSort s
-          | _ -> t
-          with Not_found -> t)
+              _, DefinedSort s -> mkSort s
+            | _ -> t
+        with Not_found -> t)
     | _ -> t
 
 let rec set_impredicative u s scstr =
-  match snd (find_univ u scstr) with
+  match UniverseMap.find u scstr with
     | DefinedSort s' ->
         if family_of_sort s = family_of_sort s' then scstr
         else failwith "sort constraint inconsistency"
@@ -214,7 +210,7 @@ let rec set_impredicative u s scstr =
           (List.fold_left (fun g u' -> set_impredicative u' s g) scstr ul)
 
 let rec set_predicative u s scstr =
-  match snd (find_univ u scstr) with
+  match UniverseMap.find u scstr with
     | DefinedSort s' ->
         if family_of_sort s = family_of_sort s' then scstr
         else failwith "sort constraint inconsistency"
@@ -242,6 +238,7 @@ let new_sort_var cstr =
   let u = Termops.new_univ() in
   (u, UniverseMap.add u (SortVar([],[])) cstr)
 
+
 let set_leq_sort (u1,(leq1,geq1)) (u2,(leq2,geq2)) scstr =
   let rec search_rec (is_b, betw, not_betw) u1 =
     if List.mem u1 betw then (true, betw, not_betw)
@@ -264,9 +261,11 @@ let set_leq_sort (u1,(leq1,geq1)) (u2,(leq2,geq2)) scstr =
     UniverseMap.add u1 (SortVar(u2::leq1,geq1))
       (UniverseMap.add u2 (SortVar(leq2, u1::geq2)) scstr)
 
-let set_leq_var u1 u2 scstr =
-  let (cu1,c1) = find_univ u1 scstr in
-  let (cu2,c2) = find_univ u2 scstr in
+let set_leq s1 s2 scstr =
+  let u1 = var_of_sort s1 in
+  let u2 = var_of_sort s2 in
+  let (cu1,c1) = canonical_find u1 scstr in
+  let (cu2,c2) = canonical_find u2 scstr in
   if cu1=cu2 then scstr
   else
     match c1,c2 with
@@ -278,31 +277,6 @@ let set_leq_var u1 u2 scstr =
       | DefinedSort(Type _ as s), _ -> set_predicative u2 s scstr
       | DefinedSort(Prop _), _ -> scstr
 
-let set_leq s1 s2 scstr =
-  let u1 = var_of_sort s1 in
-  let u2 = var_of_sort s2 in
-    set_leq_var u1 u2 scstr
-
-let set_eq_sort (u1,(leq1,geq1)) u2 scstr =
-  UniverseMap.add u1 (EqSort u2)
-    (List.fold_left (fun g u -> set_leq_var u u2 g) 
-	(List.fold_left (fun g u -> set_leq_var u2 u g) scstr geq1) leq1)
-
-let set_eq s1 s2 scstr = 
-  let u1 = var_of_sort s1 in
-  let u2 = var_of_sort s2 in
-  let (cu1,c1) = find_univ u1 scstr in
-  let (cu2,c2) = find_univ u2 scstr in
-  if cu1=cu2 then scstr
-  else
-    match c1,c2 with
-        (EqSort _, _ | _, EqSort _) -> assert false
-      | SortVar(leq1,geq1), _ ->
-          set_eq_sort (cu1,(leq1,geq1)) cu2 scstr
-      | _, SortVar(leq2,geq2) ->
-          set_eq_sort (cu2,(leq2,geq2)) cu1 scstr
-      | DefinedSort s, DefinedSort s' -> scstr
-
 let set_sort_variable s1 s2 scstr =
   let u = var_of_sort s1 in
   match s2 with
@@ -341,12 +315,8 @@ module EvarMap = struct
   let eq_evar_map x y = x == y ||
     (EvarInfoMap.equal eq_evar_info (fst x) (fst y) &&
       UniverseMap.equal (=) (snd x) (snd y))
-  let constraints (sigma,sm) = sm
-  let merge_constraints sm sm' =
-    UniverseMap.fold (fun u cstr sm -> UniverseMap.add u cstr sm) sm' sm
-  let merge (sigma,sm) (sigma',sm') = 
-    let ev = EvarInfoMap.fold (fun n v sigma -> EvarInfoMap.add sigma n v) sigma' sigma in
-      (ev,merge_constraints sm sm')
+
+  let merge e e' = fold (fun n v sigma -> add sigma n v) e' e
   
 end
  
@@ -509,10 +479,11 @@ let subst_evar_info s evi =
       evar_body = subst_evb evi.evar_body }
 
 let subst_evar_defs_light sub evd =
+  assert (UniverseMap.is_empty (snd evd.evars));
   assert (evd.conv_pbs = []);
   { evd with
-    metas = Metamap.map (map_clb (subst_mps sub)) evd.metas;
-    evars = ExistentialMap.map (subst_evar_info sub)  (fst evd.evars), (snd evd.evars);
+      metas = Metamap.map (map_clb (subst_mps sub)) evd.metas;
+      evars = ExistentialMap.map (subst_evar_info sub)  (fst evd.evars), snd evd.evars
   }
 
 let subst_evar_map = subst_evar_defs_light
@@ -531,9 +502,7 @@ let empty =  {
   metas=Metamap.empty 
 }
 
-let evars_reset_evd evd d = {d with evars = (fst evd.evars, 
-					    EvarMap.merge_constraints (snd evd.evars) (snd d.evars))}
-
+let evars_reset_evd evd d = {d with evars = evd.evars}
 let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs}
 let evar_source evk d =
   try List.assoc evk d.history
@@ -603,9 +572,6 @@ let extract_changed_conv_pbs evd p =
 let extract_all_conv_pbs evd =
   extract_conv_pbs evd (fun _ -> true)
 
-let solve_sort_cstrs cstrs = (* TODO: Check validity *)
-  UniverseMap.empty
-
 (* spiwack: should it be replaced by Evd.merge? *)
 let evar_merge evd evars =
   { evd with evars = EvarMap.merge evd.evars evars.evars }
@@ -621,41 +587,9 @@ let is_sort_variable {evars=(_,sm)} s =
 let whd_sort_variable {evars=(_,sm)} t = whd_sort_var sm t
 let set_leq_sort_variable ({evars=(sigma,sm)}as d) u1 u2 =
   { d with evars = (sigma, set_leq u1 u2 sm) }
-let set_eq_sort_variable ({evars=(sigma,sm)}as d) u1 u2 =
-  { d with evars = (sigma, set_eq u1 u2 sm) }
 let define_sort_variable ({evars=(sigma,sm)}as d) u s =
   { d with evars = (sigma, set_sort_variable u s sm) }
 let pr_sort_constraints {evars=(_,sm)} = pr_sort_cstrs sm
-let solve_sort_constraints ({evars=(sigma,sm)} as d) =
-  { d with evars = (sigma, solve_sort_cstrs sm) }
-let clear_sort_constraints ({evars=(sigma,sm)} as d) =
-  { d with evars = (sigma, UniverseMap.empty) }
-
-(* This refreshes universes in types introducing sort variables;
-   works only for inferred types (i.e. for
-   types of the form (x1:A1)...(xn:An)B with B a sort or an atom in
-   head normal form) *)
-let universes_to_variables_gen strict evd t =
-  let modified = ref false in
-  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 not (is_sort_variable !evdref us) then
-	  let s', evd = new_sort_variable !evdref in
-	  let evd = 
-	    if not (Univ.is_univ_variable u) then
-	      set_leq_sort_variable evd us s'
-	    else evd
-	  in
-	    evdref := evd; modified := true; mkSort s'
-	else t
-    | Prod (na,u,v) -> mkProd (na,u,refresh v)
-    | _ -> t in
-  let t' = refresh t in
-  if !modified then !evdref, t' else evd, t
-
-let universes_to_variables = universes_to_variables_gen false
-let universes_to_variables_strict = universes_to_variables_gen true
 
 (**********************************************************)
 (* Accessing metas *)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 10ea2ca4dd..e5cf8e2690 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -240,12 +240,7 @@ val new_sort_variable : evar_defs -> sorts * evar_defs
 val is_sort_variable : evar_defs -> sorts -> bool
 val whd_sort_variable : evar_defs -> constr -> constr
 val set_leq_sort_variable : evar_defs -> sorts -> sorts -> evar_defs
-val set_eq_sort_variable : evar_defs -> sorts -> sorts -> evar_defs
 val define_sort_variable : evar_defs -> sorts -> sorts -> evar_defs
-val solve_sort_constraints : evar_defs -> evar_defs
-val clear_sort_constraints : evar_defs -> evar_defs
-
-val universes_to_variables : evar_defs -> types -> evar_defs * types
 
 (*********************************************************************)
 (* constr with holes *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 6c58e247a5..7f5bf4ece6 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -55,10 +55,6 @@ let abstract_list_all env evd typ c l =
 
 (**)
 
-let get_type_of_with_variables env evd c =
-  let t = Retyping.get_type_of ~refresh:false env evd c in
-    Evd.universes_to_variables evd t
-
 (* A refinement of [conv_pb]: the integers tells how many arguments
    were applied in the context of the conversion problem; if the number
    is non zero, steps of eta-expansion will be allowed
@@ -174,31 +170,19 @@ let oracle_order env cf1 cf2 =
       match cf2 with
       | None -> Some true
       | Some k2 -> Some (Conv_oracle.oracle_order k1 k2)
-
-let is_trans_fconv_pb pb flags env sigma m n =
-  let sigma' = clear_sort_constraints sigma in
-    is_trans_fconv (conv_pb_of pb) flags env sigma' m n
-
-let occur_meta_or_sortvar evd c =
-  let rec occrec c = match kind_of_term c with
-    | Meta _ -> raise Occur
-    | Sort (Type u) -> raise Occur
-    | _ -> iter_constr occrec c
-  in try occrec c; false with Occur -> true
-
-
+	    
 let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flags m n =
   let trivial_unify curenv pb (sigma,metasubst,_) m n =
     let subst = if flags.use_metas_eagerly then metasubst else ms in
-    match subst_defined_metas subst m, subst_defined_metas subst n with
-    | Some m1, Some n1 ->
+    match subst_defined_metas subst m with
+    | Some m1 ->
 	if (match flags.modulo_conv_on_closed_terms with
 	    Some flags ->
-	      is_trans_fconv_pb pb flags env sigma m1 n1
+	      is_trans_fconv (conv_pb_of pb) flags env sigma m1 n
 	  | None -> false) then true else
-	  let evd = create_evar_defs sigma in
-            if not (is_ground_term evd m1) || not (is_ground_term evd n1)
-	    then false else error_cannot_unify curenv sigma (m, n)
+        if (not (is_ground_term (create_evar_defs sigma) m1))
+            || occur_meta_or_existential n then false else
+               error_cannot_unify curenv sigma (m, n)
     | _ -> false in
   let rec unirec_rec (curenv,nb as curenvnb) pb b ((sigma,metasubst,evarsubst) as substn) curm curn =
     let cM = Evarutil.whd_castappevar sigma curm
@@ -277,14 +261,12 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 	| _ ->
 	    try canonical_projections curenvnb pb b cM cN substn
 	    with ex when precatchable_exception ex ->
-              let (unif,sigma') = Evarconv.constr_unify_with_sorts sigma (conv_pb_of cv_pb) cM cN in
-		if unif then (sigma',metasubst,evarsubst)
-		else
-		  let (f1,l1) = 
-		    match kind_of_term cM with App (f,l) -> (f,l) | _ -> (cM,[||]) in
-		  let (f2,l2) =
-		    match kind_of_term cN with App (f,l) -> (f,l) | _ -> (cN,[||]) in
-		    expand curenvnb pb b substn cM f1 l1 cN f2 l2
+              if constr_cmp (conv_pb_of cv_pb) cM cN then substn else
+		let (f1,l1) = 
+		  match kind_of_term cM with App (f,l) -> (f,l) | _ -> (cM,[||]) in
+		let (f2,l2) =
+		  match kind_of_term cN with App (f,l) -> (f,l) | _ -> (cN,[||]) in
+		  expand curenvnb pb b substn cM f1 l1 cN f2 l2
 
   and expand (curenv,_ as curenvnb) pb b (sigma, _, _ as substn) cM f1 l1 cN f2 l2 =
     if trivial_unify curenv pb substn cM cN then substn
@@ -368,19 +350,19 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
       unirec_rec curenvnb pb b substn c1 (applist (c,(List.rev ks)))
 
   in
-    if (if occur_meta_or_sortvar sigma m || occur_meta_or_sortvar sigma n then false else
-      if (match flags.modulo_conv_on_closed_terms with
-      | Some flags ->
-	  is_trans_fconv_pb cv_pb flags env sigma m n
-      | None -> fst (Evarconv.constr_unify_with_sorts sigma (conv_pb_of cv_pb) m n)) then true else
+    if (if occur_meta m then false else
+       if (match flags.modulo_conv_on_closed_terms with
+	  Some flags ->
+	    is_trans_fconv (conv_pb_of cv_pb) flags env sigma m n
+	| None -> constr_cmp (conv_pb_of cv_pb) m n) then true else
       if (not (is_ground_term (create_evar_defs sigma) m))
-        || occur_meta_or_existential n then false else
-	if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
-        | Some (cv_id, cv_k), (dl_id, dl_k) ->
-            Idpred.subset dl_id cv_id && Cpred.subset dl_k cv_k
-        | None,(dl_id, dl_k) ->
-            Idpred.is_empty dl_id && Cpred.is_empty dl_k)
-	then error_cannot_unify env sigma (m, n) else false) 
+          || occur_meta_or_existential n then false else
+      if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
+            | Some (cv_id, cv_k), (dl_id, dl_k) ->
+                Idpred.subset dl_id cv_id && Cpred.subset dl_k cv_k
+            | None,(dl_id, dl_k) ->
+                Idpred.is_empty dl_id && Cpred.is_empty dl_k)
+      then error_cannot_unify env sigma (m, n) else false) 
     then subst
     else 
       unirec_rec (env,0) cv_pb conv_at_top subst m n
@@ -559,24 +541,27 @@ let w_coerce_to_type env evd c cty mvty =
     try_to_coerce env evd c cty tycon
 
 let w_coerce env evd mv c =
-  let evd,cty = get_type_of_with_variables env evd c in
+  let cty = get_type_of env evd c in
   let mvty = Typing.meta_type evd mv in
   w_coerce_to_type env evd c cty mvty
 
 let unify_to_type env sigma flags c status u =
-  let sigma, t = get_type_of_with_variables env sigma c in
+  let c = refresh_universes c in
+  let t = get_type_of env sigma c in
   let t = Tacred.hnf_constr env sigma (nf_betaiota sigma (nf_meta sigma t)) in
   let u = Tacred.hnf_constr env sigma u in
-    if status = IsSuperType then
-      unify_0 env sigma Cumul flags u t
-    else if status = IsSubType then
-      unify_0 env sigma Cumul flags t u
-    else (* If the terms were convertible under an app, 
-	    the types could be in any inclusion order *)
-      try unify_0 env sigma Cumul flags t u
-      with ex when precatchable_exception ex ->
+    try 
+      if status = IsSuperType then
 	unify_0 env sigma Cumul flags u t
-
+      else if status = IsSubType then
+	unify_0 env sigma Cumul flags t u
+      else 
+	try unify_0 env sigma Cumul flags t u
+	with e when precatchable_exception e ->
+	  unify_0 env sigma Cumul flags u t
+    with e when precatchable_exception e ->
+      (sigma,[],[])
+	
 let unify_type env sigma flags mv status c =
   let mvty = Typing.meta_type sigma mv in
   if occur_meta_or_existential mvty or is_arity env sigma mvty then
@@ -641,7 +626,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),([],[])),eqns@[(mv,status,c)]
+	      ((evd,c),([],[])),(mv,status,c)::eqns
 	  else 
 	    ((evd,c),([],[])),eqns in
 	  if meta_defined evd mv then
@@ -695,15 +680,19 @@ let w_unify_meta_types env ?(flags=default_unify_flags) evd =
    [clenv_typed_unify M N clenv] expects in addition that expected
    types of metavars are unifiable with the types of their instances    *)
 
-let check_types env flags (sigma,ms,es as subst) m n =
-  if isEvar_or_Meta (fst (whd_stack sigma m)) ||
-    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
-	(nf_betaiota sigma mt) (nf_betaiota sigma nt)
+let check_types env flags (sigma,_,_ as subst) m n =
+  if isEvar_or_Meta (fst (whd_stack sigma m)) then
+    unify_0_with_initial_metas subst true env Cumul
+      flags
+      (Retyping.get_type_of env sigma n)
+      (Retyping.get_type_of env sigma m)
+  else if isEvar_or_Meta (fst (whd_stack sigma n)) then
+    unify_0_with_initial_metas subst true env Cumul
+      flags
+      (Retyping.get_type_of env sigma m)
+      (Retyping.get_type_of env sigma n)
   else subst
-    
+
 let w_unify_core_0 env with_types cv_pb flags m n evd =
   let (mc1,evd') = retract_coercible_metas evd in
   let (sigma,ms,es) = check_types env flags (evd,mc1,[]) m n in
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 8df0858910..addf12ca13 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -73,11 +73,11 @@ let clenv_pose_dependent_evars with_evars clenv =
 
 let clenv_refine with_evars ?(with_classes=true) clenv gls =
   let clenv = clenv_pose_dependent_evars with_evars clenv in
-  let evd = Evd.solve_sort_constraints clenv.evd in
   let evd' = 
     if with_classes then 
-      Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env evd 
-    else evd
+      Typeclasses.resolve_typeclasses ~fail:(not with_evars) 
+	clenv.env clenv.evd 
+    else clenv.evd
   in
   tclTHEN
     (tclEVARS ( evd'))