Merge branch 'v8.5' into trunk

18 files changed, 181 insertions, 197 deletions

diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index d22abff10..063c9cf12 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -227,7 +227,7 @@ let judge_of_cast env c ct k expected_type =
       default_conv ~l2r:true CUMUL env ct expected_type
     | NATIVEcast ->
       let sigma = Nativelambda.empty_evars in
-      native_conv CUMUL sigma env ct expected_type
+      Nativeconv.native_conv CUMUL sigma env ct expected_type
   with NotConvertible ->
     error_actual_type env (make_judge c ct) expected_type
 
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index d0aa96fd1..7ae66c485 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -16,21 +16,21 @@ open Nativecode
 
 (** This module implements the conversion test by compiling to OCaml code *)
 
-let rec conv_val env pb lvl cu v1 v2 = 
-  if v1 == v2 then ()
+let rec conv_val env pb lvl v1 v2 cu =
+  if v1 == v2 then cu
   else
     match kind_of_value v1, kind_of_value v2 with
     | Vfun f1, Vfun f2 ->
 	let v = mk_rel_accu lvl in
-	conv_val env CONV (lvl+1) cu (f1 v) (f2 v)
+	conv_val env CONV (lvl+1) (f1 v) (f2 v) cu
     | Vfun f1, _ ->
-	conv_val env CONV lvl cu v1 (fun x -> v2 x)
+	conv_val env CONV lvl v1 (fun x -> v2 x) cu
     | _, Vfun f2 ->
-	conv_val env CONV lvl cu (fun x -> v1 x) v2
+	conv_val env CONV lvl (fun x -> v1 x) v2 cu
     | Vaccu k1, Vaccu k2 ->
-	conv_accu env pb lvl cu k1 k2
+	conv_accu env pb lvl k1 k2 cu
     | Vconst i1, Vconst i2 -> 
-	if not (Int.equal i1 i2) then raise NotConvertible
+	if Int.equal i1 i2 then cu else raise NotConvertible
     | Vblock b1, Vblock b2 ->
 	let n1 = block_size b1 in
         let n2 = block_size b2 in
@@ -38,76 +38,76 @@ let rec conv_val env pb lvl cu v1 v2 =
 	  raise NotConvertible;
 	let rec aux lvl max b1 b2 i cu =
 	  if Int.equal i max then 
-	    conv_val env CONV lvl cu (block_field b1 i) (block_field b2 i)
+	    conv_val env CONV lvl (block_field b1 i) (block_field b2 i) cu
 	  else
-	      (conv_val env CONV lvl cu (block_field b1 i) (block_field b2 i);
-	    aux lvl max b1 b2 (i+1) cu)
+	    let cu = conv_val env CONV lvl (block_field b1 i) (block_field b2 i) cu in
+	    aux lvl max b1 b2 (i+1) cu
 	in
 	aux lvl (n1-1) b1 b2 0 cu
     | Vaccu _, _ | Vconst _, _ | Vblock _, _ -> raise NotConvertible
 
-and conv_accu env pb lvl cu k1 k2 = 
+and conv_accu env pb lvl k1 k2 cu =
   let n1 = accu_nargs k1 in
   let n2 = accu_nargs k2 in
   if not (Int.equal n1 n2) then raise NotConvertible;
   if Int.equal n1 0 then 
     conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu
   else
-    (conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu;
-    List.iter2 (conv_val env CONV lvl cu) (args_of_accu k1) (args_of_accu k2))
+    let cu = conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu in
+    List.fold_right2 (conv_val env CONV lvl) (args_of_accu k1) (args_of_accu k2) cu
 
 and conv_atom env pb lvl a1 a2 cu =
-  if a1 == a2 then ()
+  if a1 == a2 then cu
   else
     match a1, a2 with
     | Ameta _, _ | _, Ameta _ | Aevar _, _ | _, Aevar _ -> assert false
     | Arel i1, Arel i2 -> 
-	if not (Int.equal i1 i2) then raise NotConvertible
+	if Int.equal i1 i2 then cu else raise NotConvertible
     | Aind ind1, Aind ind2 ->
-	if not (eq_puniverses eq_ind ind1 ind2) then raise NotConvertible
+	if eq_puniverses eq_ind ind1 ind2 then cu else raise NotConvertible
     | Aconstant c1, Aconstant c2 ->
-	if not (eq_puniverses eq_constant c1 c2) then raise NotConvertible
+	if eq_puniverses eq_constant c1 c2 then cu else raise NotConvertible
     | Asort s1, Asort s2 -> 
-        check_sort_cmp_universes env pb s1 s2 cu
+        sort_cmp_universes env pb s1 s2 cu
     | Avar id1, Avar id2 ->
-	if not (Id.equal id1 id2) then raise NotConvertible
+	if Id.equal id1 id2 then cu else raise NotConvertible
     | Acase(a1,ac1,p1,bs1), Acase(a2,ac2,p2,bs2) ->
 	if not (eq_ind a1.asw_ind a2.asw_ind) then raise NotConvertible;
-	conv_accu env CONV lvl cu ac1 ac2;
+	let cu = conv_accu env CONV lvl ac1 ac2 cu in
 	let tbl = a1.asw_reloc in
 	let len = Array.length tbl in
-	if Int.equal len 0 then conv_val env CONV lvl cu p1 p2
+	if Int.equal len 0 then conv_val env CONV lvl p1 p2 cu
 	else begin
-	  conv_val env CONV lvl cu p1 p2;
-	  let max = len - 1 in
-	  let rec aux i =
-	    let tag,arity = tbl.(i) in
-	    let ci = 
-	      if Int.equal arity 0 then mk_const tag
-	      else mk_block tag (mk_rels_accu lvl arity) in
-	    let bi1 = bs1 ci and bi2 = bs2 ci in
-	    if Int.equal i max then conv_val env CONV (lvl + arity) cu bi1 bi2
-	    else (conv_val env CONV (lvl + arity) cu bi1 bi2; aux (i+1)) in
-	  aux 0
+	    let cu = conv_val env CONV lvl p1 p2 cu in
+	    let max = len - 1 in
+	    let rec aux i cu =
+	      let tag,arity = tbl.(i) in
+	      let ci =
+		if Int.equal arity 0 then mk_const tag
+		else mk_block tag (mk_rels_accu lvl arity) in
+	      let bi1 = bs1 ci and bi2 = bs2 ci in
+	      if Int.equal i max then conv_val env CONV (lvl + arity) bi1 bi2 cu
+	      else aux (i+1) (conv_val env CONV (lvl + arity) bi1 bi2 cu) in
+	    aux 0 cu
 	  end
     | Afix(t1,f1,rp1,s1), Afix(t2,f2,rp2,s2) ->
 	if not (Int.equal s1 s2) || not (Array.equal Int.equal rp1 rp2) then raise NotConvertible;
-	if f1 == f2 then ()
+	if f1 == f2 then cu
 	else conv_fix env lvl t1 f1 t2 f2 cu
     | (Acofix(t1,f1,s1,_) | Acofixe(t1,f1,s1,_)),
       (Acofix(t2,f2,s2,_) | Acofixe(t2,f2,s2,_)) ->
 	if not (Int.equal s1 s2) then raise NotConvertible;
-	if f1 == f2 then ()
+	if f1 == f2 then cu
 	else
 	  if not (Int.equal (Array.length f1) (Array.length f2)) then raise NotConvertible
 	  else conv_fix env lvl t1 f1 t2 f2 cu 
     | Aprod(_,d1,c1), Aprod(_,d2,c2) ->
-	conv_val env CONV lvl cu d1 d2;
-	let v = mk_rel_accu lvl in
-	conv_val env pb (lvl + 1) cu (d1 v) (d2 v)
+       let cu = conv_val env CONV lvl d1 d2 cu in
+       let v = mk_rel_accu lvl in
+       conv_val env pb (lvl + 1) (d1 v) (d2 v) cu
     | Aproj(p1,ac1), Aproj(p2,ac2) ->
        if not (Constant.equal p1 p2) then raise NotConvertible
-       else conv_accu env CONV lvl cu ac1 ac2
+       else conv_accu env CONV lvl ac1 ac2 cu
     | Arel _, _ | Aind _, _ | Aconstant _, _ | Asort _, _ | Avar _, _
     | Acase _, _ | Afix _, _ | Acofix _, _ | Acofixe _, _ | Aprod _, _
     | Aproj _, _ -> raise NotConvertible
@@ -118,21 +118,15 @@ and conv_fix env lvl t1 f1 t2 f2 cu =
   let max = len - 1 in
   let fargs = mk_rels_accu lvl len in
   let flvl = lvl + len in
-  let rec aux i =
-    conv_val env CONV lvl cu t1.(i) t2.(i);
+  let rec aux i cu =
+    let cu = conv_val env CONV lvl t1.(i) t2.(i) cu in
     let fi1 = napply f1.(i) fargs in
     let fi2 = napply f2.(i) fargs in
-    if Int.equal i max then conv_val env CONV flvl cu fi1 fi2
-    else (conv_val env CONV flvl cu fi1 fi2; aux (i+1)) in
-  aux 0
+    if Int.equal i max then conv_val env CONV flvl fi1 fi2 cu
+    else aux (i+1) (conv_val env CONV flvl fi1 fi2 cu) in
+  aux 0 cu
 
-let native_conv pb sigma env t1 t2 =
-  if Coq_config.no_native_compiler then begin
-    let msg = "Native compiler is disabled, falling back to VM conversion test." in
-    Pp.msg_warning (Pp.str msg);
-    vm_conv pb env t1 t2
-  end
-  else
+let native_conv_gen pb sigma env univs t1 t2 =
   let penv = Environ.pre_env env in 
   let ml_filename, prefix = get_ml_filename () in
   let code, upds = mk_conv_code penv sigma prefix t1 t2 in
@@ -146,8 +140,25 @@ let native_conv pb sigma env t1 t2 =
         let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
         if !Flags.debug then Pp.msg_debug (Pp.str time_info);
         (* TODO change 0 when we can have deBruijn *)
-        conv_val env pb 0 (Environ.universes env) !rt1 !rt2
+        fst (conv_val env pb 0 !rt1 !rt2 univs)
       end
   | _ -> anomaly (Pp.str "Compilation failure") 
 
-let _ = set_nat_conv native_conv
+(* Wrapper for [native_conv] above *)
+let native_conv cv_pb sigma env t1 t2 =
+  if Coq_config.no_native_compiler then begin
+    let msg = "Native compiler is disabled, falling back to VM conversion test." in
+    Pp.msg_warning (Pp.str msg);
+    vm_conv cv_pb env t1 t2
+  end
+  else
+  let univs = Environ.universes env in
+  let b =
+    if cv_pb = CUMUL then Constr.leq_constr_univs univs t1 t2
+    else Constr.eq_constr_univs univs t1 t2
+  in
+  if not b then
+    let univs = (univs, checked_universes) in
+    let t1 = Term.it_mkLambda_or_LetIn t1 (Environ.rel_context env) in
+    let t2 = Term.it_mkLambda_or_LetIn t2 (Environ.rel_context env) in
+    let _ = native_conv_gen cv_pb sigma env univs t1 t2 in ()
diff --git a/kernel/nativeconv.mli b/kernel/nativeconv.mli
index 318a7d830..4dddb9fd3 100644
--- a/kernel/nativeconv.mli
+++ b/kernel/nativeconv.mli
@@ -12,3 +12,7 @@ open Nativelambda
 (** This module implements the conversion test by compiling to OCaml code *)
 
 val native_conv : conv_pb -> evars -> types conversion_function
+
+(** A conversion function parametrized by a universe comparator. Used outside of
+    the kernel. *)
+val native_conv_gen : conv_pb -> evars -> (types, 'a) generic_conversion_function
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 6e1c3c5b7..e081870ba 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -26,8 +26,6 @@ open Environ
 open Closure
 open Esubst
 
-let left2right = ref false
-
 let rec is_empty_stack = function
   [] -> true
   | Zupdate _::s -> is_empty_stack s
@@ -208,9 +206,7 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv =
           let cu1 = cmp_rec s1 s2 cuniv in
           (match (z1,z2) with
             | (Zlapp a1,Zlapp a2) -> 
-	      if !left2right then
-		Array.fold_left2 (fun cu x y -> f x y cu) cu1 a1 a2
-	      else Array.fold_right2 f a1 a2 cu1
+	       Array.fold_right2 f a1 a2 cu1
 	    | (Zlproj (c1,l1),Zlproj (c2,l2)) -> 
 	      if not (eq_constant c1 c2) then 
 		raise NotConvertible
@@ -632,7 +628,7 @@ let infer_cmp_universes env pb s0 s1 univs =
 let infer_convert_instances flex u u' (univs,cstrs) =
   (univs, Univ.enforce_eq_instances u u' cstrs)
 
-let infered_universes : (UGraph.t * Univ.Constraint.t) universe_compare = 
+let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare = 
   { compare = infer_cmp_universes;
     compare_instances = infer_convert_instances }
 
@@ -665,7 +661,7 @@ let trans_conv_universes ?(l2r=false) ?(evars=fun _->None) reds =
 let trans_conv_leq_universes ?(l2r=false) ?(evars=fun _->None) reds = 
   trans_fconv_universes reds CUMUL l2r evars
 
-let fconv = trans_fconv (Id.Pred.full, Cpred.full)
+let fconv = trans_fconv full_transparent_state
 
 let conv_cmp ?(l2r=false) cv_pb = fconv cv_pb l2r (fun _->None)
 let conv ?(l2r=false) ?(evars=fun _->None) = fconv CONV l2r evars
@@ -680,7 +676,7 @@ let conv_leq_vecti ?(l2r=false) ?(evars=fun _->None) env v1 v2 =
     v1
     v2
 
-let generic_conv cv_pb l2r evars reds env univs t1 t2 =
+let generic_conv cv_pb ~l2r evars reds env univs t1 t2 =
   let (s, _) = 
     clos_fconv reds cv_pb l2r evars env univs t1 t2 
   in s
@@ -692,7 +688,7 @@ let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 =
   in
     if b then cstrs
     else
-      let univs = ((univs, Univ.Constraint.empty), infered_universes) in
+      let univs = ((univs, Univ.Constraint.empty), inferred_universes) in
       let ((_,cstrs), _) = clos_fconv reds cv_pb l2r evars env univs t1 t2 in
 	cstrs
 
@@ -711,19 +707,7 @@ let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_sta
     env univs t1 t2 = 
   infer_conv_universes CUMUL l2r evars ts env univs t1 t2
 
-(* option for conversion *)
-let nat_conv = ref (fun cv_pb sigma ->
-		    fconv cv_pb false (sigma.Nativelambda.evars_val))
-let set_nat_conv f = nat_conv := f
-
-let native_conv cv_pb sigma env t1 t2 =
-  if eq_constr t1 t2 then ()
-  else begin
-    let t1 = (it_mkLambda_or_LetIn t1 (rel_context env)) in
-    let t2 = (it_mkLambda_or_LetIn t2 (rel_context env)) in
-    !nat_conv cv_pb sigma env t1 t2 
-  end
-
+(* This reference avoids always having to link C code with the kernel *)
 let vm_conv = ref (fun cv_pb -> fconv cv_pb false (fun _->None))
 let set_vm_conv f = vm_conv := f
 let vm_conv cv_pb env t1 t2 =
@@ -734,11 +718,7 @@ let vm_conv cv_pb env t1 t2 =
     fconv cv_pb false (fun _->None) env t1 t2
 
 let default_conv cv_pb ?(l2r=false) env t1 t2 =
-  try
     fconv cv_pb false (fun _ -> None) env t1 t2
-  with Not_found | Invalid_argument _ ->
-    Pp.msg_warning (Pp.str "Compilation failed, falling back to standard conversion");
-    fconv cv_pb false (fun _->None) env t1 t2
 
 let default_conv_leq = default_conv CUMUL
 (*
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 2c1c0ec05..0bb855c67 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -10,8 +10,6 @@ open Term
 open Context
 open Environ
 
-val left2right : bool ref
-
 (***********************************************************************
   s Reduction functions *)
 
@@ -49,14 +47,11 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a
 
 type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.constraints
 
-val check_sort_cmp_universes :
-  env -> conv_pb -> sorts -> sorts -> UGraph.t -> unit
-
-(* val sort_cmp : *)
-(*     conv_pb -> sorts -> sorts -> Univ.constraints -> Univ.constraints *)
+val sort_cmp_universes : env -> conv_pb -> sorts -> sorts ->
+  'a * 'a universe_compare -> 'a * 'a universe_compare
 
-(* val conv_sort      : sorts conversion_function *)
-(* val conv_sort_leq  : sorts conversion_function *)
+val checked_universes : UGraph.t universe_compare
+val inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare
 
 val trans_conv_cmp       : ?l2r:bool -> conv_pb -> constr trans_conversion_function
 val trans_conv           :
@@ -77,22 +72,20 @@ val conv_leq       :
 val conv_leq_vecti :
   ?l2r:bool -> ?evars:(existential->constr option) -> types array conversion_function
 
+(** These conversion functions are used by module subtyping, which needs to infer
+    universe constraints inside the kernel *)
 val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) -> 
   ?ts:Names.transparent_state -> constr infer_conversion_function
 val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> 
   ?ts:Names.transparent_state -> types infer_conversion_function
 
-val generic_conv : conv_pb -> bool -> (existential->constr option) -> 
+val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) ->
   Names.transparent_state -> (constr,'a) generic_conversion_function
 
 (** option for conversion *)
 val set_vm_conv : (conv_pb -> types conversion_function) -> unit
 val vm_conv : conv_pb -> types conversion_function
 
-val set_nat_conv :
-  (conv_pb -> Nativelambda.evars -> types conversion_function) -> unit
-val native_conv : conv_pb -> Nativelambda.evars -> types conversion_function
-
 val default_conv     : conv_pb -> ?l2r:bool -> types conversion_function
 val default_conv_leq : ?l2r:bool -> types conversion_function
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 8895bae5d..09299f31d 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -300,7 +300,7 @@ let judge_of_cast env cj k tj =
       match k with
       | VMcast ->
           mkCast (cj.uj_val, k, expected_type),
-          vm_conv CUMUL env cj.uj_type expected_type
+          Reduction.vm_conv CUMUL env cj.uj_type expected_type
       | DEFAULTcast ->
           mkCast (cj.uj_val, k, expected_type),
           default_conv ~l2r:false CUMUL env cj.uj_type expected_type
@@ -310,7 +310,7 @@ let judge_of_cast env cj k tj =
       | NATIVEcast ->
 	 let sigma = Nativelambda.empty_evars in
          mkCast (cj.uj_val, k, expected_type),
-         native_conv CUMUL sigma env cj.uj_type expected_type
+         Nativeconv.native_conv CUMUL sigma env cj.uj_type expected_type
     in
       { uj_val = c;
 	uj_type = expected_type }
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 27e184ea3..2f6be0601 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -46,7 +46,7 @@ let rec conv_val env pb k v1 v2 cu =
 
 and conv_whd env pb k whd1 whd2 cu =
   match whd1, whd2 with
-  | Vsort s1, Vsort s2 -> check_sort_cmp_universes env pb s1 s2 cu; cu
+  | Vsort s1, Vsort s2 -> sort_cmp_universes env pb s1 s2 cu
   | Vprod p1, Vprod p2 ->
       let cu = conv_val env CONV k (dom p1) (dom p2) cu in
       conv_fun env pb k (codom p1) (codom p2) cu
@@ -163,67 +163,25 @@ let rec eq_puniverses f (x,l1) (y,l2) cu =
 and conv_universes l1 l2 cu =
   if Univ.Instance.equal l1 l2 then cu else raise NotConvertible
 
-let rec conv_eq env pb t1 t2 cu =
-  if t1 == t2 then cu
-  else
-    match kind_of_term t1, kind_of_term t2 with
-    | Rel n1, Rel n2 ->
-	if Int.equal n1 n2 then cu else raise NotConvertible
-    | Meta m1, Meta m2 ->
-	if Int.equal m1 m2 then cu else raise NotConvertible
-    | Var id1, Var id2 ->
-	if Id.equal id1 id2 then cu else raise NotConvertible
-    | Sort s1, Sort s2 -> check_sort_cmp_universes env pb s1 s2 cu; cu
-    | Cast (c1,_,_), _ -> conv_eq env pb c1 t2 cu
-    | _, Cast (c2,_,_) -> conv_eq env pb t1 c2 cu
-    | Prod (_,t1,c1), Prod (_,t2,c2) ->
-	conv_eq env pb c1 c2 (conv_eq env CONV t1 t2 cu)
-    | Lambda (_,t1,c1), Lambda (_,t2,c2) -> conv_eq env CONV c1 c2 cu
-    | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) ->
-	conv_eq env pb c1 c2 (conv_eq env CONV b1 b2 cu)
-    | App (c1,l1), App (c2,l2) ->
-	conv_eq_vect env l1 l2 (conv_eq env CONV c1 c2 cu)
-    | Evar (e1,l1), Evar (e2,l2) ->
-	if Evar.equal e1 e2 then conv_eq_vect env l1 l2 cu
-	else raise NotConvertible
-    | Const c1, Const c2 -> eq_puniverses eq_constant c1 c2 cu
-    | Proj (p1,c1), Proj (p2,c2) ->
-	if eq_constant (Projection.constant p1) (Projection.constant p2) then
-	  conv_eq env pb c1 c2 cu 
-	else raise NotConvertible
-    | Ind c1, Ind c2 ->
-       eq_puniverses eq_ind c1 c2 cu
-    | Construct c1, Construct c2 ->
-       eq_puniverses eq_constructor c1 c2 cu
-    | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
-	let pcu = conv_eq env CONV p1 p2 cu in
-	let ccu = conv_eq env CONV c1 c2 pcu in
-	conv_eq_vect env bl1 bl2 ccu
-    | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) ->
-	if Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 then conv_eq_vect env tl1 tl2 (conv_eq_vect env bl1 bl2 cu)
-	else raise NotConvertible
-    | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
-	if Int.equal ln1 ln2 then conv_eq_vect env tl1 tl2 (conv_eq_vect env bl1 bl2 cu)
-	else raise NotConvertible
-    | _ -> raise NotConvertible
-
-and conv_eq_vect env vt1 vt2 cu =
-  let len = Array.length vt1 in
-  if Int.equal len (Array.length vt2) then
-    let rcu = ref cu in
-    for i = 0 to len-1 do
-      rcu := conv_eq env CONV vt1.(i) vt2.(i) !rcu
-    done; !rcu
-  else raise NotConvertible
-
-let vconv pb env t1 t2 =
-  let _cu =
-    try conv_eq env pb t1 t2 (universes env)
-    with NotConvertible ->
-      let v1 = val_of_constr env t1 in
-      let v2 = val_of_constr env t2 in
-      let cu = conv_val env pb (nb_rel env) v1 v2 (universes env) in
-      cu
-  in ()
-
-let _ = Reduction.set_vm_conv vconv
+let vm_conv_gen cv_pb env univs t1 t2 =
+  try 
+    let v1 = val_of_constr env t1 in
+    let v2 = val_of_constr env t2 in
+    fst (conv_val env cv_pb (nb_rel env) v1 v2 univs)
+  with Not_found | Invalid_argument _ ->
+    (Pp.msg_warning
+      (Pp.str "Bytecode compilation failed, falling back to default conversion");
+     Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
+			    full_transparent_state env univs t1 t2)
+
+let vm_conv cv_pb env t1 t2 =
+  let univs = Environ.universes env in
+  let b =
+    if cv_pb = CUMUL then Constr.leq_constr_univs univs t1 t2
+    else Constr.eq_constr_univs univs t1 t2
+  in
+  if not b then
+    let univs = (univs, checked_universes) in
+    let _ = vm_conv_gen cv_pb env univs t1 t2 in ()
+
+let _ = Reduction.set_vm_conv vm_conv
diff --git a/kernel/vconv.mli b/kernel/vconv.mli
index 1a29a4d51..49e5d23e6 100644
--- a/kernel/vconv.mli
+++ b/kernel/vconv.mli
@@ -12,7 +12,11 @@ open Reduction
 
 (**********************************************************************
   s conversion functions *)
-val vconv : conv_pb -> types conversion_function
+val vm_conv : conv_pb -> types conversion_function
 
-val val_of_constr : env -> constr -> values
+(** A conversion function parametrized by a universe comparator. Used outside of
+    the kernel. *)
+val vm_conv_gen : conv_pb -> (types, 'a) generic_conversion_function
 
+(** Precompute a VM value from a constr *)
+val val_of_constr : env -> constr -> values
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 2432b8d29..dafe88d8d 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -22,11 +22,6 @@ open Nativelambda
 
 (** This module implements normalization by evaluation to OCaml code *)
 
-let evars_of_evar_map evd =
-  { evars_val = Evd.existential_opt_value evd;
-    evars_typ = Evd.existential_type evd;
-    evars_metas = Evd.meta_type evd }
-
 exception Find_at of int
 
 let invert_tag cst tag reloc_tbl =
@@ -375,11 +370,17 @@ and  nf_predicate env ind mip params v pT =
       true, mkLambda(name,dom,body)
   | _, _ -> false, nf_type env v
 
+let evars_of_evar_map sigma =
+  { Nativelambda.evars_val = Evd.existential_opt_value sigma;
+    Nativelambda.evars_typ = Evd.existential_type sigma;
+    Nativelambda.evars_metas = Evd.meta_type sigma }
+
 let native_norm env sigma c ty =  
   if Coq_config.no_native_compiler then
     error "Native_compute reduction has been disabled at configure time."
   else
-  let penv = Environ.pre_env env in 
+  let penv = Environ.pre_env env in
+  let sigma = evars_of_evar_map sigma in
   (*
   Format.eprintf "Numbers of free variables (named): %i\n" (List.length vl1);
   Format.eprintf "Numbers of free variables (rel): %i\n" (List.length vl2);
@@ -400,3 +401,10 @@ let native_norm env sigma c ty =
         if !Flags.debug then Pp.msg_debug (Pp.str time_info);
         res
     | _ -> anomaly (Pp.str "Compilation failure") 
+
+let native_conv_generic pb sigma t =
+  Nativeconv.native_conv_gen pb (evars_of_evar_map sigma) t
+
+let native_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 =
+  Reductionops.infer_conv_gen (fun pb ~l2r sigma ts -> native_conv_generic pb sigma)
+    ~catch_incon:true ~pb env sigma t1 t2
diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli
index c854e8c9c..035203838 100644
--- a/pretyping/nativenorm.mli
+++ b/pretyping/nativenorm.mli
@@ -12,6 +12,8 @@ open Nativelambda
 
 (** This module implements normalization by evaluation to OCaml code *)
 
-val evars_of_evar_map : evar_map -> evars
+val native_norm : env -> evar_map -> constr -> types -> constr
 
-val native_norm : env -> evars -> constr -> types -> constr
+(** Conversion with inference of universe constraints *)
+val native_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr ->
+  evar_map * bool
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index bb21b87d3..c2cf1f83d 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -929,25 +929,20 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
  	    let cj = pretype empty_tycon env evdref lvar c in
 	    let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in
 	      if not (occur_existential cty || occur_existential tval) then
-		begin 
-		  try
-		    let env = Environ.push_context_set (Evd.universe_context_set !evdref) env in 
-		    ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj
-		  with Reduction.NotConvertible -> 
-		    error_actual_type_loc loc env !evdref cj tval 
+		let (evd,b) = Reductionops.vm_infer_conv env !evdref cty tval in
+		if b then (evdref := evd; cj)
+		else
+		  error_actual_type_loc loc env !evdref cj tval 
                       (ConversionFailed (env,cty,tval))
-		end
 	      else user_err_loc (loc,"",str "Cannot check cast with vm: " ++
 		str "unresolved arguments remain.")
 	  | NATIVEcast ->
  	    let cj = pretype empty_tycon env evdref lvar c in
 	    let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in
-            let evars = Nativenorm.evars_of_evar_map !evdref in
-	    let env = Environ.push_context_set (Evd.universe_context_set !evdref) env in 
             begin
-              try
-                ignore (Nativeconv.native_conv Reduction.CUMUL evars env cty tval); cj
-              with Reduction.NotConvertible -> 
+	      let (evd,b) = Nativenorm.native_infer_conv env !evdref cty tval in
+	      if b then (evdref := evd; cj)
+	      else
                 error_actual_type_loc loc env !evdref cj tval 
                   (ConversionFailed (env,cty,tval))
             end
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index dc70f36cc..bb1bc7d2e 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1251,9 +1251,6 @@ let pb_equal = function
   | Reduction.CUMUL -> Reduction.CONV
   | Reduction.CONV -> Reduction.CONV
 
-let sort_cmp cv_pb s1 s2 u = 
-  Reduction.check_sort_cmp_universes cv_pb s1 s2 u
-
 let test_trans_conversion (f: ?l2r:bool-> ?evars:'a->'b) reds env sigma x y =
   try
     let evars ev = safe_evar_value sigma ev in
@@ -1295,8 +1292,8 @@ let sigma_univ_state =
   { Reduction.compare = sigma_compare_sorts;
     Reduction.compare_instances = sigma_compare_instances }
 
-let infer_conv ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) 
-    env sigma x y = 
+let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
+    ?(ts=full_transparent_state) env sigma x y =
   try 
     let b, sigma = 
       let b, cstrs = 
@@ -1313,14 +1310,23 @@ let infer_conv ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_s
       if b then sigma, true
       else
 	let sigma' = 
-	  Reduction.generic_conv pb false (safe_evar_value sigma) ts 
+	  conv_fun pb ~l2r:false sigma ts
 	    env (sigma, sigma_univ_state) x y in
 	  sigma', true
   with
   | Reduction.NotConvertible -> sigma, false
   | Univ.UniverseInconsistency _ when catch_incon -> sigma, false
   | e when is_anomaly e -> error "Conversion test raised an anomaly"
-    
+
+let infer_conv = infer_conv_gen (fun pb ~l2r sigma ->
+      Reduction.generic_conv pb ~l2r (safe_evar_value sigma))
+
+(* This reference avoids always having to link C code with the kernel *)
+let vm_infer_conv = ref (infer_conv ~catch_incon:true ~ts:full_transparent_state)
+let set_vm_infer_conv f = vm_infer_conv := f
+let vm_infer_conv ?(pb=Reduction.CUMUL) env t1 t2 =
+  !vm_infer_conv ~pb env t1 t2
+
 (********************************************************************)
 (*             Special-Purpose Reduction                            *)
 (********************************************************************)
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 5e1c467c8..d5a844847 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -251,8 +251,6 @@ type conversion_test = constraints -> constraints
 val pb_is_equal : conv_pb -> bool
 val pb_equal : conv_pb -> conv_pb
 
-val sort_cmp : env -> conv_pb -> sorts -> sorts -> UGraph.t -> unit
-
 val is_conv : env ->  evar_map -> constr -> constr -> bool
 val is_conv_leq : env ->  evar_map -> constr -> constr -> bool
 val is_fconv : conv_pb -> env ->  evar_map -> constr -> constr -> bool
@@ -266,7 +264,7 @@ val is_trans_fconv : conv_pb -> transparent_state -> env ->  evar_map -> constr
  *)
 val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env ->  evar_map -> constr -> constr -> bool
 
-(** [infer_fconv] Adds necessary universe constraints to the evar map.
+(** [infer_conv] Adds necessary universe constraints to the evar map.
     pb defaults to CUMUL and ts to a full transparent state.
     @raises UniverseInconsistency iff catch_incon is set to false, 
     otherwise returns false in that case.
@@ -274,6 +272,20 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env ->  evar_map -> con
 val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> 
   env -> evar_map -> constr -> constr -> evar_map * bool
 
+(** Conversion with inference of universe constraints *)
+val set_vm_infer_conv : (?pb:conv_pb -> env -> evar_map -> constr -> constr ->
+  evar_map * bool) -> unit
+val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr ->
+  evar_map * bool
+
+
+(** [infer_conv_gen] behaves like [infer_conv] but is parametrized by a
+conversion function. Used to pretype vm and native casts. *)
+val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> transparent_state ->
+    (constr, evar_map) Reduction.generic_conversion_function) ->
+  ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> env ->
+  evar_map -> constr -> constr -> evar_map * bool
+
 (** {6 Special-Purpose Reduction Functions } *)
 
 val whd_meta : evar_map -> constr -> constr
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index f768e4fee..46af784dd 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -312,3 +312,9 @@ and nf_cofix env cf =
 let cbv_vm env c t  =
   let v = Vconv.val_of_constr env c in
   nf_val env v t
+
+let vm_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 =
+  Reductionops.infer_conv_gen (fun pb ~l2r sigma ts -> Vconv.vm_conv_gen pb)
+    ~catch_incon:true ~pb env sigma t1 t2
+
+let _ = Reductionops.set_vm_infer_conv vm_infer_conv
diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli
index 7dabbc6cb..9421b2d85 100644
--- a/pretyping/vnorm.mli
+++ b/pretyping/vnorm.mli
@@ -8,7 +8,7 @@
 
 open Term
 open Environ
+open Evd
 
 (** {6 Reduction functions } *)
 val cbv_vm : env -> constr -> types -> constr
-
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index f172bbdd1..be92f2b04 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -35,8 +35,7 @@ let cbv_native env sigma c =
     cbv_vm env sigma c
   else
     let ctyp = Retyping.get_type_of env sigma c in
-    let evars = Nativenorm.evars_of_evar_map sigma in
-    Nativenorm.native_norm env evars c ctyp
+    Nativenorm.native_norm env sigma c ctyp
 
 let whd_cbn flags env sigma t =
   let (state,_) =
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 96c7d79ca..2755ed9cb 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -458,7 +458,9 @@ module Hint_db = struct
     else List.exists (matches_mode args) modes
 
   let merge_entry db nopat pat =
-    let h = Sort.merge pri_order (List.map snd db.hintdb_nopat @ nopat) pat in
+    let h = List.sort pri_order_int (List.map snd db.hintdb_nopat) in
+    let h = List.merge pri_order_int h nopat in
+    let h = List.merge pri_order_int h pat in
     List.map realize_tac h
 
   let map_none db =
@@ -562,7 +564,9 @@ module Hint_db = struct
 
   let remove_one gr db = remove_list [gr] db
 
-  let get_entry se = List.map realize_tac (se.sentry_nopat @ se.sentry_pat)
+  let get_entry se =
+    let h = List.merge pri_order_int se.sentry_nopat se.sentry_pat in
+    List.map realize_tac h
 
   let iter f db =
     let iter_se k se = f (Some k) se.sentry_mode (get_entry se) in
diff --git a/test-suite/bugs/closed/4346.v b/test-suite/bugs/closed/4346.v
new file mode 100644
index 000000000..b50dff241
--- /dev/null
+++ b/test-suite/bugs/closed/4346.v
@@ -0,0 +1,2 @@
+Check (Set <: Type).
+Check (Set <<: Type).