- Use transparency information all the way through unification and

conversion.
- Fix trans_fconv* to use evars correctly.
- Normalize the goal with respect to evars before rewriting in
[rewrite], allowing to see instanciations from other subgoals.


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

6 files changed, 150 insertions, 256 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index df0fc161a..84b6c7b94 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -25,11 +25,11 @@ type flex_kind_of_term =
   | MaybeFlexible of constr
   | Flexible of existential
 
-let flex_kind_of_term c l =
+let flex_kind_of_term ts c l =
   match kind_of_term c with
-    | Const _ -> MaybeFlexible c
+    | Const n when is_transparent_constant ts n -> MaybeFlexible c
     | Rel n -> MaybeFlexible c
-    | Var id -> MaybeFlexible c
+    | Var id when is_transparent_variable ts id -> MaybeFlexible c
     | Lambda _ when l<>[] -> MaybeFlexible c
     | LetIn _  -> MaybeFlexible c
     | Evar ev -> Flexible ev
@@ -157,16 +157,15 @@ let ise_array2 evd f v1 v2 =
   if lv1 = Array.length v2 then allrec evd (pred lv1)
   else (evd,false)
 
-let rec evar_conv_x env evd pbty term1 term2 =
-  let sigma =  evd in
-  let term1 = whd_head_evar sigma term1 in
-  let term2 = whd_head_evar sigma term2 in
+let rec evar_conv_x ts env evd pbty term1 term2 =
+  let term1 = whd_head_evar evd term1 in
+  let term2 = whd_head_evar evd term2 in
   (* Maybe convertible but since reducing can erase evars which [evar_apprec]
      could have found, we do it only if the terms are free of evar.
      Note: incomplete heuristic... *)
   let ground_test =
     if is_ground_term evd term1 && is_ground_term evd term2 then
-      if is_fconv pbty env evd term1 term2 then
+      if is_trans_fconv pbty ts env evd term1 term2 then
         Some true
       else if is_ground_env evd env then Some false
       else None
@@ -179,40 +178,40 @@ let rec evar_conv_x env evd pbty term1 term2 =
         let term1 = apprec_nohdbeta env evd term1 in
         let term2 = apprec_nohdbeta env evd term2 in
         if is_undefined_evar evd term1 then
-          solve_simple_eqn evar_conv_x env evd
+          solve_simple_eqn (evar_conv_x ts) env evd
 	    (position_problem true pbty,destEvar term1,term2)
         else if is_undefined_evar evd term2 then
-          solve_simple_eqn evar_conv_x env evd
+          solve_simple_eqn (evar_conv_x ts) env evd
 	    (position_problem false pbty,destEvar term2,term1)
         else
-          evar_eqappr_x env evd pbty
+          evar_eqappr_x ts env evd pbty
             (decompose_app term1) (decompose_app term2)
 
-and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
+and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
   (* Evar must be undefined since we have flushed evars *)
-  match (flex_kind_of_term term1 l1, flex_kind_of_term term2 l2) with
+  match (flex_kind_of_term ts term1 l1, flex_kind_of_term ts term2 l2) with
     | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) ->
 	let f1 i =
 	  if List.length l1 > List.length l2 then
             let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
             ise_and i
-              [(fun i -> solve_simple_eqn evar_conv_x env i
+              [(fun i -> solve_simple_eqn (evar_conv_x ts) env i
 	        (position_problem false pbty,ev2,applist(term1,deb1)));
               (fun i -> ise_list2 i
-                  (fun i -> evar_conv_x env i CONV) rest1 l2)]
+                  (fun i -> evar_conv_x ts env i CONV) rest1 l2)]
 	  else
 	    let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
             ise_and i
-              [(fun i -> solve_simple_eqn evar_conv_x env i
+              [(fun i -> solve_simple_eqn (evar_conv_x ts) env i
 	          (position_problem true pbty,ev1,applist(term2,deb2)));
               (fun i -> ise_list2 i
-                  (fun i -> evar_conv_x env i CONV) l1 rest2)]
+                  (fun i -> evar_conv_x ts env i CONV) l1 rest2)]
 	and f2 i =
           if sp1 = sp2 then
             ise_and i
             [(fun i -> ise_list2 i
-                  (fun i -> evar_conv_x env i CONV) l1 l2);
-             (fun i -> solve_refl evar_conv_x env i sp1 al1 al2,
+                  (fun i -> evar_conv_x ts env i CONV) l1 l2);
+             (fun i -> solve_refl (evar_conv_x ts) env i sp1 al1 al2,
                   true)]
           else (i,false)
 	in
@@ -228,7 +227,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	    (* Preserve generality (except that CCI has no eta-conversion) *)
 	    let t2 = nf_evar evd (applist appr2) in
 	    let t2 = solve_pattern_eqn env l1 t2 in
-	    solve_simple_eqn evar_conv_x env evd
+	    solve_simple_eqn (evar_conv_x ts) env evd
 	      (position_problem true pbty,ev1,t2)
 	  else if
             List.length l1 <= List.length l2
@@ -240,13 +239,13 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
             ise_and i
               (* First compare extra args for better failure message *)
               [(fun i -> ise_list2 i
-                  (fun i -> evar_conv_x env i CONV) l1 rest2);
-               (fun i -> evar_conv_x env i pbty term1 (applist(term2,deb2)))]
+                  (fun i -> evar_conv_x ts env i CONV) l1 rest2);
+               (fun i -> evar_conv_x ts env i pbty term1 (applist(term2,deb2)))]
           else (i,false)
 	and f2 i =
 	  match eval_flexible_term env flex2 with
 	    | Some v2 ->
-		evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2)
+		evar_eqappr_x ts env i pbty appr1 (evar_apprec env i l2 v2)
 	    | None -> (i,false)
 	in
 	ise_try evd [f1; f2]
@@ -261,7 +260,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	    (* Preserve generality (except that CCI has no eta-conversion) *)
 	    let t1 = nf_evar evd (applist appr1) in
 	    let t1 = solve_pattern_eqn env l2 t1 in
-	    solve_simple_eqn evar_conv_x env evd
+	    solve_simple_eqn (evar_conv_x ts) env evd
 	      (position_problem false pbty,ev2,t1)
 	  else if
        	    List.length l2 <= List.length l1
@@ -272,13 +271,13 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
             ise_and i
             (* First compare extra args for better failure message *)
               [(fun i -> ise_list2 i
-                  (fun i -> evar_conv_x env i CONV) rest1 l2);
-               (fun i -> evar_conv_x env i pbty (applist(term1,deb1)) term2)]
+                  (fun i -> evar_conv_x ts env i CONV) rest1 l2);
+               (fun i -> evar_conv_x ts env i pbty (applist(term1,deb1)) term2)]
           else (i,false)
 	and f2 i =
 	  match eval_flexible_term env flex1 with
 	    | Some v1 ->
-		evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2
+		evar_eqappr_x ts env i pbty (evar_apprec env i l1 v1) appr2
 	    | None -> (i,false)
 	in
 	ise_try evd [f1; f2]
@@ -286,11 +285,11 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
     | MaybeFlexible flex1, MaybeFlexible flex2 ->
 	let f1 i =
 	  if flex1 = flex2 then
-	    ise_list2 i (fun i -> evar_conv_x env i CONV) l1 l2
+	    ise_list2 i (fun i -> evar_conv_x ts env i CONV) l1 l2
 	  else
 	     (i,false)
 	and f2 i =
-	  (try conv_record env i
+	  (try conv_record ts env i
              (try check_conv_record appr1 appr2
 	      with Not_found -> check_conv_record appr2 appr1)
            with Not_found -> (i,false))
@@ -303,20 +302,20 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  then
 	    match eval_flexible_term env flex1 with
 	    | Some v1 ->
-		evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2
+		evar_eqappr_x ts env i pbty (evar_apprec env i l1 v1) appr2
 	    | None ->
 		match eval_flexible_term env flex2 with
 		| Some v2 ->
-		    evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2)
+		    evar_eqappr_x ts env i pbty appr1 (evar_apprec env i l2 v2)
 		| None -> (i,false)
 	  else
 	    match eval_flexible_term env flex2 with
 	    | Some v2 ->
-		evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2)
+		evar_eqappr_x ts env i pbty appr1 (evar_apprec env i l2 v2)
 	    | None ->
 		match eval_flexible_term env flex1 with
 		| Some v1 ->
-		    evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2
+		    evar_eqappr_x ts env i pbty (evar_apprec env i l1 v1) appr2
 		| None -> (i,false)
 	in
 	ise_try evd [f1; f2; f3]
@@ -329,7 +328,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	let env' = push_rel (na,None,c) env in
         let appr1 = evar_apprec env' evd [] c'1 in
 	let appr2 = (lift 1 term2, List.map (lift 1) l2 @ [mkRel 1]) in
-	evar_eqappr_x env' evd CONV appr1 appr2
+	evar_eqappr_x ts env' evd CONV appr1 appr2
 
     | (Flexible _ | MaybeFlexible _), Rigid c2 when isLambda c2 ->
 	assert (l2 = []);
@@ -338,7 +337,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	let env' = push_rel (na,None,c) env in
 	let appr1 = (lift 1 term1, List.map (lift 1) l1 @ [mkRel 1]) in
         let appr2 = evar_apprec env' evd [] c'2 in
-	evar_eqappr_x env' evd CONV appr1 appr2
+	evar_eqappr_x ts env' evd CONV appr1 appr2
 
     | Flexible ev1, Rigid _ ->
 	if
@@ -349,7 +348,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  (* Preserve generality (except that CCI has no eta-conversion) *)
 	  let t2 = nf_evar evd (applist appr2) in
 	  let t2 = solve_pattern_eqn env l1 t2 in
-	  solve_simple_eqn evar_conv_x env evd
+	  solve_simple_eqn (evar_conv_x ts) env evd
 	    (position_problem true pbty,ev1,t2)
 	else
 	  (* Postpone the use of an heuristic *)
@@ -365,7 +364,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  (* Preserve generality (except that CCI has no eta-conversion) *)
 	  let t1 = nf_evar evd (applist appr1) in
 	  let t1 = solve_pattern_eqn env l2 t1 in
-	  solve_simple_eqn evar_conv_x env evd
+	  solve_simple_eqn (evar_conv_x ts) env evd
 	    (position_problem false pbty,ev2,t1)
 	else
 	  (* Postpone the use of an heuristic *)
@@ -374,116 +373,116 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 
     | MaybeFlexible flex1, Rigid _ ->
 	let f3 i =
-	  (try conv_record env i (check_conv_record appr1 appr2)
+	  (try conv_record ts env i (check_conv_record appr1 appr2)
            with Not_found -> (i,false))
 	and f4 i =
 	  match eval_flexible_term env flex1 with
 	    | Some v1 ->
- 		evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2
+ 		evar_eqappr_x ts env i pbty (evar_apprec env i l1 v1) appr2
 	    | None -> (i,false)
 	in
 	ise_try evd [f3; f4]
 
     | Rigid _ , MaybeFlexible flex2 ->
 	let f3 i =
-	  (try conv_record env i (check_conv_record appr2 appr1)
+	  (try conv_record ts env i (check_conv_record appr2 appr1)
            with Not_found -> (i,false))
 	and f4 i =
 	  match eval_flexible_term env flex2 with
 	    | Some v2 ->
- 		evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2)
+ 		evar_eqappr_x ts env i pbty appr1 (evar_apprec env i l2 v2)
 	    | None -> (i,false)
 	in
 	ise_try evd [f3; f4]
 
     | Rigid c1, Rigid c2 -> match kind_of_term c1, kind_of_term c2 with
 
-	| Cast (c1,_,_), _ -> evar_eqappr_x env evd pbty (c1,l1) appr2
+	| Cast (c1,_,_), _ -> evar_eqappr_x ts env evd pbty (c1,l1) appr2
 
-	| _, Cast (c2,_,_) -> evar_eqappr_x env evd pbty appr1 (c2,l2)
+	| _, Cast (c2,_,_) -> evar_eqappr_x ts env evd pbty appr1 (c2,l2)
 
 	| Sort s1, Sort s2 when l1=[] & l2=[] ->
-            (evd,base_sort_cmp pbty s1 s2)
+	    (evd, base_sort_cmp pbty s1 s2)
 
 	| Lambda (na,c1,c'1), Lambda (_,c2,c'2) ->
 	    assert (l1=[] & l2=[]);
             ise_and evd
-              [(fun i -> evar_conv_x env i CONV c1 c2);
+              [(fun i -> evar_conv_x ts env i CONV c1 c2);
                (fun i ->
                  let c = nf_evar i c1 in
-                 evar_conv_x (push_rel (na,None,c) env) i CONV c'1 c'2)]
+                 evar_conv_x ts (push_rel (na,None,c) env) i CONV c'1 c'2)]
 
 	| LetIn (na,b1,t1,c'1), LetIn (_,b2,_,c'2) ->
 	    let f1 i =
               ise_and i
-                [(fun i -> evar_conv_x env i CONV b1 b2);
+                [(fun i -> evar_conv_x ts env i CONV b1 b2);
                  (fun i ->
                    let b = nf_evar i b1 in
 	           let t = nf_evar i t1 in
-                   evar_conv_x (push_rel (na,Some b,t) env) i pbty c'1 c'2);
+                   evar_conv_x ts (push_rel (na,Some b,t) env) i pbty c'1 c'2);
                  (fun i -> ise_list2 i
-                     (fun i -> evar_conv_x env i CONV) l1 l2)]
+                     (fun i -> evar_conv_x ts env i CONV) l1 l2)]
 	    and f2 i =
               let appr1 = evar_apprec env i l1 (subst1 b1 c'1)
               and appr2 = evar_apprec env i l2 (subst1 b2 c'2)
-	      in evar_eqappr_x env i pbty appr1 appr2
+	      in evar_eqappr_x ts env i pbty appr1 appr2
 	    in
 	    ise_try evd [f1; f2]
 
 	| LetIn (_,b1,_,c'1), _ ->(* On fait commuter les args avec le Let *)
 	     let appr1 = evar_apprec env evd l1 (subst1 b1 c'1)
-             in evar_eqappr_x env evd pbty appr1 appr2
+             in evar_eqappr_x ts env evd pbty appr1 appr2
 
 	| _, LetIn (_,b2,_,c'2) ->
 	    let appr2 = evar_apprec env evd l2 (subst1 b2 c'2)
-            in evar_eqappr_x env evd pbty appr1 appr2
+            in evar_eqappr_x ts env evd pbty appr1 appr2
 
 	| Prod (n,c1,c'1), Prod (_,c2,c'2) when l1=[] & l2=[] ->
             ise_and evd
-              [(fun i -> evar_conv_x env i CONV c1 c2);
+              [(fun i -> evar_conv_x ts env i CONV c1 c2);
                (fun i ->
  	         let c = nf_evar i c1 in
-	         evar_conv_x (push_rel (n,None,c) env) i pbty c'1 c'2)]
+	         evar_conv_x ts (push_rel (n,None,c) env) i pbty c'1 c'2)]
 
 	| Ind sp1, Ind sp2 ->
 	    if eq_ind sp1 sp2 then
-              ise_list2 evd (fun i -> evar_conv_x env i CONV) l1 l2
+              ise_list2 evd (fun i -> evar_conv_x ts env i CONV) l1 l2
             else (evd, false)
 
 	| Construct sp1, Construct sp2 ->
 	    if eq_constructor sp1 sp2 then
-              ise_list2 evd (fun i -> evar_conv_x env i CONV) l1 l2
+              ise_list2 evd (fun i -> evar_conv_x ts env i CONV) l1 l2
             else (evd, false)
 
 	| Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
             ise_and evd
-              [(fun i -> evar_conv_x env i CONV p1 p2);
-               (fun i -> evar_conv_x env i CONV c1 c2);
+              [(fun i -> evar_conv_x ts env i CONV p1 p2);
+               (fun i -> evar_conv_x ts env i CONV c1 c2);
 	       (fun i -> ise_array2 i
-                   (fun i -> evar_conv_x env i CONV) cl1 cl2);
-               (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) l1 l2)]
+                   (fun i -> evar_conv_x ts env i CONV) cl1 cl2);
+               (fun i -> ise_list2 i (fun i -> evar_conv_x ts env i CONV) l1 l2)]
 
 	| Fix (li1,(_,tys1,bds1 as recdef1)), Fix (li2,(_,tys2,bds2)) ->
             if li1=li2 then
               ise_and evd
                 [(fun i -> ise_array2 i
-                    (fun i -> evar_conv_x env i CONV) tys1 tys2);
+                    (fun i -> evar_conv_x ts env i CONV) tys1 tys2);
                  (fun i -> ise_array2 i
-		     (fun i -> evar_conv_x (push_rec_types recdef1 env) i CONV)
+		     (fun i -> evar_conv_x ts (push_rec_types recdef1 env) i CONV)
 		     bds1 bds2);
 	         (fun i -> ise_list2 i
-                     (fun i -> evar_conv_x env i CONV) l1 l2)]
+                     (fun i -> evar_conv_x ts env i CONV) l1 l2)]
 	    else (evd,false)
 	| CoFix (i1,(_,tys1,bds1 as recdef1)), CoFix (i2,(_,tys2,bds2)) ->
             if i1=i2  then
               ise_and evd
                 [(fun i -> ise_array2 i
-                    (fun i -> evar_conv_x env i CONV) tys1 tys2);
+                    (fun i -> evar_conv_x ts env i CONV) tys1 tys2);
                  (fun i -> ise_array2 i
-		     (fun i -> evar_conv_x (push_rec_types recdef1 env) i CONV)
+		     (fun i -> evar_conv_x ts (push_rec_types recdef1 env) i CONV)
 		     bds1 bds2);
                  (fun i -> ise_list2 i
-                     (fun i -> evar_conv_x env i CONV) l1 l2)]
+                     (fun i -> evar_conv_x ts env i CONV) l1 l2)]
             else (evd,false)
 
 	(* Eta-expansion *)
@@ -493,7 +492,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	    let env' = push_rel (na,None,c) env in
             let appr1 = evar_apprec env' evd [] c'1 in
 	    let appr2 = (lift 1 c2, List.map (lift 1) l2 @ [mkRel 1]) in
-	    evar_eqappr_x env' evd CONV appr1 appr2
+	    evar_eqappr_x ts env' evd CONV appr1 appr2
 
 	| _, Lambda (na,c2,c'2) ->
 	    assert (l2 = []);
@@ -501,7 +500,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	    let env' = push_rel (na,None,c) env in
 	    let appr1 = (lift 1 c1, List.map (lift 1) l1 @ [mkRel 1]) in
             let appr2 = evar_apprec env' evd [] c'2 in
-	    evar_eqappr_x env' evd CONV appr1 appr2
+	    evar_eqappr_x ts env' evd CONV appr1 appr2
 
 	| (Meta _ | Ind _ | Construct _ | Sort _ | Prod _), _ -> (evd,false)
 	| _, (Meta _ | Ind _ | Construct _ | Sort _ | Prod _) -> (evd,false)
@@ -512,7 +511,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	| (Rel _ | Var _ | Const _ | Evar _), _ -> assert false
 	| _, (Rel _ | Var _ | Const _ | Evar _) -> assert false
 
-and conv_record env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
+and conv_record trs env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
   let (evd',ks,_) =
     List.fold_left
       (fun (i,ks,m) b ->
@@ -525,29 +524,29 @@ and conv_record env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
   ise_and evd'
     [(fun i ->
        ise_list2 i
-         (fun i x1 x -> evar_conv_x env i CONV x1 (substl ks x))
+         (fun i x1 x -> evar_conv_x trs env i CONV x1 (substl ks x))
          params1 params);
     (fun i ->
       ise_list2 i
-        (fun i u1 u -> evar_conv_x env i CONV u1 (substl ks u))
+        (fun i u1 u -> evar_conv_x trs env i CONV u1 (substl ks u))
         us2 us);
-    (fun i -> evar_conv_x env i CONV c1 (applist (c,(List.rev ks))));
-    (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) ts ts1)]
+    (fun i -> evar_conv_x trs env i CONV c1 (applist (c,(List.rev ks))));
+    (fun i -> ise_list2 i (fun i -> evar_conv_x trs env i CONV) ts ts1)]
 
 (* We assume here |l1| <= |l2| *)
 
-let first_order_unification env evd (ev1,l1) (term2,l2) =
+let first_order_unification ts env evd (ev1,l1) (term2,l2) =
   let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
   ise_and evd
     (* First compare extra args for better failure message *)
-    [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) rest2 l1);
+    [(fun i -> ise_list2 i (fun i -> evar_conv_x ts env i CONV) rest2 l1);
     (fun i ->
       (* Then instantiate evar unless already done by unifying args *)
       let t2 = applist(term2,deb2) in
       if is_defined_evar i ev1 then
-	evar_conv_x env i CONV t2 (mkEvar ev1)
+	evar_conv_x ts env i CONV t2 (mkEvar ev1)
       else
-	solve_simple_eqn ~choose:true evar_conv_x env i (None,ev1,t2))]
+	solve_simple_eqn ~choose:true (evar_conv_x ts) env i (None,ev1,t2))]
 
 let choose_less_dependent_instance evk evd term args =
   let evi = Evd.find_undefined evd evk in
@@ -556,7 +555,7 @@ let choose_less_dependent_instance evk evd term args =
   if subst' = [] then error "Too complex unification problem." else
   Evd.define evk (mkVar (fst (List.hd subst'))) evd
 
-let apply_conversion_problem_heuristic env evd pbty t1 t2 =
+let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
   let t1 = apprec_nohdbeta env evd (whd_head_evar evd t1) in
   let t2 = apprec_nohdbeta env evd (whd_head_evar evd t2) in
   let (term1,l1 as appr1) = decompose_app t1 in
@@ -574,19 +573,19 @@ let apply_conversion_problem_heuristic env evd pbty t1 t2 =
       choose_less_dependent_instance evk2 evd term1 args2, true
   | Evar ev1,_ when List.length l1 <= List.length l2 ->
       (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *)
-      first_order_unification env evd (ev1,l1) appr2
+      first_order_unification ts env evd (ev1,l1) appr2
   | _,Evar ev2 when List.length l2 <= List.length l1 ->
       (* On "u u1 .. u(n+p) = ?n t1 .. tn", try first-order unification *)
-      first_order_unification env evd (ev2,l2) appr1
+      first_order_unification ts env evd (ev2,l2) appr1
   | _ ->
       (* Some head evar have been instantiated, or unknown kind of problem *)
-      evar_conv_x env evd pbty t1 t2
+      evar_conv_x ts env evd pbty t1 t2
 
-let consider_remaining_unif_problems env evd =
+let consider_remaining_unif_problems ?(ts=full_transparent_state) env evd =
   let (evd,pbs) = extract_all_conv_pbs evd in
   let heuristic_solved_evd = List.fold_left
     (fun evd (pbty,env,t1,t2) ->
-      let evd', b = apply_conversion_problem_heuristic env evd pbty t1 t2 in
+      let evd', b = apply_conversion_problem_heuristic ts env evd pbty t1 t2 in
 	if b then evd' else Pretype_errors.error_cannot_unify env evd (t1, t2))
     evd pbs in
     Evd.fold_undefined (fun ev ev_info evd' -> match ev_info.evar_source with
@@ -596,22 +595,22 @@ let consider_remaining_unif_problems env evd =
 
 (* Main entry points *)
 
-let the_conv_x     env t1 t2 evd =
-  match evar_conv_x env evd CONV  t1 t2 with
+let the_conv_x ?(ts=full_transparent_state) env t1 t2 evd =
+  match evar_conv_x ts env evd CONV  t1 t2 with
       (evd',true) -> evd'
     | _ -> raise Reduction.NotConvertible
 
-let the_conv_x_leq env t1 t2 evd =
-  match evar_conv_x env evd CUMUL t1 t2 with
+let the_conv_x_leq ?(ts=full_transparent_state) env t1 t2 evd =
+  match evar_conv_x ts env evd CUMUL t1 t2 with
       (evd', true) -> evd'
     | _ -> raise Reduction.NotConvertible
 
-let e_conv env evd t1 t2 =
-  match evar_conv_x env !evd CONV t1 t2 with
+let e_conv ?(ts=full_transparent_state) env evd t1 t2 =
+  match evar_conv_x ts env !evd CONV t1 t2 with
       (evd',true) -> evd := evd'; true
     | _ -> false
 
-let e_cumul env evd t1 t2 =
-  match evar_conv_x env !evd CUMUL t1 t2 with
+let e_cumul ?(ts=full_transparent_state) env evd t1 t2 =
+  match evar_conv_x ts env !evd CUMUL t1 t2 with
       (evd',true) -> evd := evd'; true
     | _ -> false
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 18a74ff5c..e1f507b0a 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Names
 open Term
 open Sign
 open Environ
@@ -13,25 +14,25 @@ open Reductionops
 open Evd
 
 (** returns exception Reduction.NotConvertible if not unifiable *)
-val the_conv_x     : env -> constr -> constr -> evar_map -> evar_map
-val the_conv_x_leq : env -> constr -> constr -> evar_map -> evar_map
+val the_conv_x     : ?ts:transparent_state -> env -> constr -> constr -> evar_map -> evar_map
+val the_conv_x_leq : ?ts:transparent_state -> env -> constr -> constr -> evar_map -> evar_map
 
 (** The same function resolving evars by side-effect and
    catching the exception *)
-val e_conv  : env -> evar_map ref -> constr -> constr -> bool
-val e_cumul : env -> evar_map ref -> constr -> constr -> bool
+val e_conv  : ?ts:transparent_state -> env -> evar_map ref -> constr -> constr -> bool
+val e_cumul : ?ts:transparent_state -> env -> evar_map ref -> constr -> constr -> bool
 
 (**/**)
 (* For debugging *)
-val evar_conv_x :
+val evar_conv_x : transparent_state ->
   env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool
-val evar_eqappr_x :
+val evar_eqappr_x : transparent_state ->
   env -> evar_map ->
     conv_pb -> constr * constr list -> constr * constr list ->
       evar_map * bool
 (**/**)
 
-val consider_remaining_unif_problems : env -> evar_map -> evar_map
+val consider_remaining_unif_problems : ?ts:transparent_state -> env -> evar_map -> evar_map
 
 val check_conv_record : constr * types list -> constr * types list ->
   constr * constr list * (constr list * constr list) *
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 3b96a4a3b..36abd5406 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -209,139 +209,9 @@ module EvarInfoMap = struct
 
 end
 
-(*******************************************************************)
-(*                Constraints for sort variables                   *)
-(*******************************************************************)
-
-type sort_var = Univ.universe
-
-type sort_constraint =
-  | DefinedSort of sorts (* instantiated sort var *)
-  | SortVar of sort_var list * sort_var list (* (leq,geq) *)
-  | EqSort of sort_var
-
-module UniverseMap =
-  Map.Make (struct type t = Univ.universe let compare = compare end)
-
-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 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)
-    | _ -> t
-
-let rec set_impredicative u s scstr =
-  match UniverseMap.find u scstr with
-    | DefinedSort s' ->
-        if family_of_sort s = family_of_sort s' then scstr
-        else failwith "sort constraint inconsistency"
-    | EqSort u' ->
-        UniverseMap.add u (DefinedSort s) (set_impredicative u' s scstr)
-    | SortVar(_,ul) ->
-        (* also set sorts lower than u as impredicative *)
-        UniverseMap.add u (DefinedSort s)
-          (List.fold_left (fun g u' -> set_impredicative u' s g) scstr ul)
-
-let rec set_predicative u s scstr =
-  match UniverseMap.find u scstr with
-    | DefinedSort s' ->
-        if family_of_sort s = family_of_sort s' then scstr
-        else failwith "sort constraint inconsistency"
-    | EqSort u' ->
-        UniverseMap.add u (DefinedSort s) (set_predicative u' s scstr)
-    | SortVar(ul,_) ->
-        UniverseMap.add u (DefinedSort s)
-          (List.fold_left (fun g u' -> set_impredicative u' s g) scstr ul)
-
-let var_of_sort = function
-    Type u -> u
-  | _ -> assert false
-
-let is_sort_var s scstr =
-  match s with
-      Type u ->
-        (try
-          match canonical_find u scstr with
-              _, DefinedSort _ -> false
-            | _ -> true
-        with Not_found -> false)
-    | _ -> false
-
-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)
-    else if List.mem u1 not_betw then (is_b, betw, not_betw)
-    else if u1 = u2 then (true, u1::betw,not_betw) else
-      match UniverseMap.find u1 scstr with
-          EqSort u1' -> search_rec (is_b,betw,not_betw) u1'
-        | SortVar(leq,_) ->
-            let (is_b',betw',not_betw') =
-              List.fold_left search_rec (false,betw,not_betw) leq in
-            if is_b' then (true, u1::betw', not_betw')
-            else (false, betw', not_betw')
-        | DefinedSort _ -> (false,betw,u1::not_betw) in
-  let (is_betw,betw,_) = search_rec (false, [], []) u1 in
-  if is_betw then
-    UniverseMap.add u1 (SortVar(leq1@leq2,geq1@geq2))
-      (List.fold_left
-        (fun g u -> UniverseMap.add u (EqSort u1) g) scstr betw)
-  else
-    UniverseMap.add u1 (SortVar(u2::leq1,geq1))
-      (UniverseMap.add u2 (SortVar(leq2, u1::geq2)) scstr)
-
-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
-        (EqSort _, _ | _, EqSort _) -> assert false
-      | SortVar(leq1,geq1), SortVar(leq2,geq2) ->
-          set_leq_sort (cu1,(leq1,geq1)) (cu2,(leq2,geq2)) scstr
-      | _, DefinedSort(Prop _ as s) -> set_impredicative u1 s scstr
-      | _, DefinedSort(Type _) -> scstr
-      | DefinedSort(Type _ as s), _ -> set_predicative u2 s scstr
-      | DefinedSort(Prop _), _ -> scstr
-
-let set_sort_variable s1 s2 scstr =
-  let u = var_of_sort s1 in
-  match s2 with
-      Prop _ -> set_impredicative u s2 scstr
-    | Type _ -> set_predicative u s2 scstr
-
-let pr_sort_cstrs g =
-  let l = UniverseMap.fold (fun u c l -> (u,c)::l) g [] in
-  str "SORT CONSTRAINTS:" ++ fnl() ++
-  prlist_with_sep fnl (fun (u,c) ->
-    match c with
-        EqSort u' -> Univ.pr_uni u ++ str" == " ++ Univ.pr_uni u'
-      | DefinedSort s -> Univ.pr_uni u ++ str " := " ++ print_sort s
-      | SortVar(leq,geq) ->
-          str"[" ++ hov 0 (prlist_with_sep spc Univ.pr_uni geq) ++
-          str"] <= "++ Univ.pr_uni u ++ brk(0,0) ++ str"<= [" ++
-          hov 0 (prlist_with_sep spc Univ.pr_uni leq) ++ str"]")
-    l
-
 module EvarMap = struct
-  type t = EvarInfoMap.t * sort_constraints
-  let empty = EvarInfoMap.empty, UniverseMap.empty
+  type t = EvarInfoMap.t * Univ.universes
+  let empty = EvarInfoMap.empty, Univ.initial_universes
   let add (sigma,sm) k v = (EvarInfoMap.add sigma k v, sm)
   let add_undefined (sigma,sm) k v = (EvarInfoMap.add_undefined sigma k v, sm)
   let find (sigma,_) = EvarInfoMap.find sigma
@@ -364,11 +234,11 @@ module EvarMap = struct
   let progress_evar_map (sigma1,sm1 as x) (sigma2,sm2 as y) = not (x == y) &&
     (EvarInfoMap.exists_undefined sigma1
       (fun k v -> assert (v.evar_body = Evar_empty);
-        EvarInfoMap.is_defined sigma2 k)
-    || not (UniverseMap.equal (=) sm1 sm2))
+        EvarInfoMap.is_defined sigma2 k))
 
   let merge e e' = fold e' (fun n v sigma -> add sigma n v) e
-
+  let add_constraints (sigma, sm) cstrs =
+    (sigma, Univ.merge_constraints cstrs sm)
 end
 
 (*******************************************************************)
@@ -500,6 +370,8 @@ let existential_value d e = EvarMap.existential_value d.evars e
 let existential_type d e = EvarMap.existential_type d.evars e
 let existential_opt_value d e = EvarMap.existential_opt_value d.evars e
 
+let add_constraints d e = {d with evars= EvarMap.add_constraints d.evars e}
+
 (*** /Lifting... ***)
 
 (* evar_map are considered empty disregarding histories *)
@@ -519,7 +391,7 @@ 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 (Univ.initial_universes = (snd evd.evars));
   assert (evd.conv_pbs = []);
   { evd with
       metas = Metamap.map (map_clb (subst_mps sub)) evd.metas;
@@ -617,16 +489,36 @@ let evar_list evd c =
 (* Sort variables *)
 
 let new_sort_variable ({ evars = (sigma,sm) } as d)=
-  let (u,scstr) = new_sort_var sm in
-  (Type u,{ d with evars = (sigma,scstr) } )
-let is_sort_variable {evars=(_,sm)} s =
-  is_sort_var s sm
-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 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 u = Termops.new_univ() in
+    (Type u, d)
+
+let is_sort_variable {evars=(_,sm)} s = match s with Type _ -> true | _ -> false 
+let whd_sort_variable {evars=(_,sm)} t = t
+
+let univ_of_sort = function
+  | Type u -> u
+  | Prop Pos -> Univ.type0_univ
+  | Prop Null -> Univ.type0m_univ
+
+let set_leq_sort d s1 s2 =
+  if s1 = s2 then d
+  else 
+    let u1 = univ_of_sort s1 and u2 = univ_of_sort s2 in
+      match s1, s2 with
+      | Prop c, Prop c' -> 
+	  if c = Null && c' = Pos then d
+	  else (raise (Univ.UniverseInconsistency (Univ.Le, u1, u2)))
+      | _, _ ->
+	  add_constraints d (Univ.enforce_geq u2 u1 Univ.empty_constraint)
+
+let set_eq_sort d s1 s2 =
+  if s1 = s2 then d
+  else
+    let u1, u2 = univ_of_sort s1, univ_of_sort s2 in
+      match s1, s2 with
+      | Prop c, Prop c' -> raise (Univ.UniverseInconsistency (Univ.Eq, u1, u2))
+      | _, _ ->
+	  add_constraints d (Univ.enforce_eq u1 u2 Univ.empty_constraint)
 
 (**********************************************************)
 (* Accessing metas *)
@@ -823,7 +715,7 @@ let pr_evar_info evi =
   in
   hov 2 (str"["  ++ phyps ++ spc () ++ str"|- "  ++ pty ++ pb ++ str"]")
 
-let pr_evar_map_t (evars,cstrs as sigma) =
+let pr_evar_map_t (evars,univs as sigma) =
   let evs =
     if evars = EvarInfoMap.empty then mt ()
     else
@@ -833,8 +725,9 @@ let pr_evar_map_t (evars,cstrs as sigma) =
 		  h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi))
 		(EvarMap.to_list sigma))++fnl()
   and cs =
-    if cstrs = UniverseMap.empty then mt ()
-    else pr_sort_cstrs cstrs++fnl()
+    if univs = Univ.initial_universes then mt ()
+    else str"UNIVERSES:"++brk(0,1)++
+      h 0 (Univ.pr_universes univs)++fnl()
   in evs ++ cs
 
 let pr_constraints pbs =
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 751009434..8c31d6af3 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -162,6 +162,8 @@ val is_evar : evar_map -> evar -> bool
 val is_defined : evar_map -> evar -> bool
 val is_undefined : evar_map -> evar -> bool
 
+val add_constraints : evar_map -> Univ.constraints -> evar_map
+
 (** {6 ... } *)
 (** [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has
     no body and [Not_found] if it does not exist in [sigma] *)
@@ -248,8 +250,8 @@ val subst_defined_metas : metabinding list -> constr -> constr option
 val new_sort_variable : evar_map -> sorts * evar_map
 val is_sort_variable : evar_map -> sorts -> bool
 val whd_sort_variable : evar_map -> constr -> constr
-val set_leq_sort_variable : evar_map -> sorts -> sorts -> evar_map
-val define_sort_variable : evar_map -> sorts -> sorts -> evar_map
+val set_leq_sort : evar_map -> sorts -> sorts -> evar_map
+val set_eq_sort : evar_map -> sorts -> sorts -> evar_map
 
 (********************************************************************
    constr with holes *)
@@ -275,7 +277,6 @@ type unsolvability_explanation = SeveralInstancesFound of int
 
 val pr_evar_info : evar_info -> Pp.std_ppcmds
 val pr_evar_map : evar_map -> Pp.std_ppcmds
-val pr_sort_constraints : evar_map -> Pp.std_ppcmds
 val pr_metaset : Metaset.t -> Pp.std_ppcmds
 
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 689e544b8..92ad6bea6 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -605,8 +605,8 @@ let is_conv env sigma = test_conversion Reduction.conv env sigma
 let is_conv_leq env sigma = test_conversion Reduction.conv_leq env sigma
 let is_fconv = function | CONV -> is_conv | CUMUL -> is_conv_leq
 
-let test_trans_conversion f reds env sigma x y =
-  try let _ = f reds env (nf_evar sigma x) (nf_evar sigma y) in true
+let test_trans_conversion (f:?evars:'a->'b) reds env sigma x y =
+  try let _ = f ~evars:(safe_evar_value sigma) reds env x y in true
   with NotConvertible -> false
     | Anomaly _ -> error "Conversion test raised an anomaly"
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index fd287f3af..6121ba7d8 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -637,8 +637,8 @@ let order_metas metas =
 
 (* Solve an equation ?n[x1=u1..xn=un] = t where ?n is an evar *)
 
-let solve_simple_evar_eqn env evd ev rhs =
-  let evd,b = solve_simple_eqn Evarconv.evar_conv_x env evd (None,ev,rhs) in
+let solve_simple_evar_eqn ts env evd ev rhs =
+  let evd,b = solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,rhs) in
   if not b then error_cannot_unify env evd (mkEvar ev,rhs);
   Evarconv.consider_remaining_unif_problems env evd
 
@@ -669,12 +669,12 @@ let w_merge env with_types flags (evd,metas,evars) =
 		w_merge_rec evd' metas evars eqns
 	      else
 		let evd', rhs'' = pose_all_metas_as_evars env evd rhs' in
-		w_merge_rec (solve_simple_evar_eqn env evd' ev rhs'')
+		w_merge_rec (solve_simple_evar_eqn flags.modulo_delta env evd' ev rhs'')
 		  metas evars' eqns
 
           | _ ->
 	    let evd', rhs'' = pose_all_metas_as_evars env evd rhs' in
-	      w_merge_rec (solve_simple_evar_eqn env evd' ev rhs'')
+	      w_merge_rec (solve_simple_evar_eqn flags.modulo_delta env evd' ev rhs'')
 		metas evars' eqns
 	end
     | [] ->