1 files changed, 42 insertions, 41 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 38106fbf6..f4af31386 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -648,25 +648,24 @@ let check_leq univs u u' =
 
 let check_sort_cmp_universes env pb s0 s1 univs =
   let open Sorts in
-  match (s0,s1) with
+  if not (type_in_type env) then
+    match (s0,s1) with
     | (Prop c1, Prop c2) when is_cumul pb ->
       begin match c1, c2 with
-      | Null, _ | _, Pos -> () (* Prop <= Set *)
-      | _ -> raise NotConvertible
+        | Null, _ | _, Pos -> () (* Prop <= Set *)
+        | _ -> raise NotConvertible
       end
     | (Prop c1, Prop c2) -> if c1 != c2 then raise NotConvertible
     | (Prop c1, Type u) ->
-	if not (type_in_type env) then
-	let u0 = univ_of_sort s0 in
-	(match pb with
-	| CUMUL -> check_leq univs u0 u
-	| CONV -> check_eq univs u0 u)
+      let u0 = univ_of_sort s0 in
+      (match pb with
+       | CUMUL -> check_leq univs u0 u
+       | CONV -> check_eq univs u0 u)
     | (Type u, Prop c) -> raise NotConvertible
     | (Type u1, Type u2) ->
-        if not (type_in_type env) then
-	(match pb with
-	| CUMUL -> check_leq univs u1 u2
-	| CONV -> check_eq univs u1 u2)
+      (match pb with
+       | CUMUL -> check_leq univs u1 u2
+       | CONV -> check_eq univs u1 u2)
 
 let checked_sort_cmp_universes env pb s0 s1 univs =
   check_sort_cmp_universes env pb s0 s1 univs; univs
@@ -699,25 +698,25 @@ let infer_leq (univs, cstrs as cuniv) u u' =
 
 let infer_cmp_universes env pb s0 s1 univs =
   let open Sorts in
-  match (s0,s1) with
+  if type_in_type env then univs
+  else
+    match (s0,s1) with
     | (Prop c1, Prop c2) when is_cumul pb ->
       begin match c1, c2 with
-      | Null, _ | _, Pos -> univs (* Prop <= Set *)
-      | _ -> raise NotConvertible
+        | Null, _ | _, Pos -> univs (* Prop <= Set *)
+        | _ -> raise NotConvertible
       end
     | (Prop c1, Prop c2) -> if c1 == c2 then univs else raise NotConvertible
     | (Prop c1, Type u) ->
       let u0 = univ_of_sort s0 in
-	(match pb with
-	| CUMUL -> infer_leq univs u0 u
-	| CONV -> infer_eq univs u0 u)
+      (match pb with
+       | CUMUL -> infer_leq univs u0 u
+       | CONV -> infer_eq univs u0 u)
     | (Type u, Prop c) -> raise NotConvertible
     | (Type u1, Type u2) ->
-        if not (type_in_type env) then
-	(match pb with
-	| CUMUL -> infer_leq univs u1 u2
-	| CONV -> infer_eq univs u1 u2)
-        else univs
+      (match pb with
+       | CUMUL -> infer_leq univs u1 u2
+       | CONV -> infer_eq univs u1 u2)
 
 let infer_convert_instances ~flex u u' (univs,cstrs) =
   let cstrs' =
@@ -789,24 +788,6 @@ 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
 
-(* This reference avoids always having to link C code with the kernel *)
-let vm_conv = ref (fun cv_pb env ->
-		   gen_conv cv_pb env ~evars:((fun _->None), universes env))
-
-let warn_bytecode_compiler_failed =
-  let open Pp in
-  CWarnings.create ~name:"bytecode-compiler-failed" ~category:"bytecode-compiler"
-         (fun () -> strbrk "Bytecode compiler failed, " ++
-                      strbrk "falling back to standard conversion")
-
-let set_vm_conv (f:conv_pb -> types kernel_conversion_function) = vm_conv := f
-let vm_conv cv_pb env t1 t2 =
-  try
-    !vm_conv cv_pb env t1 t2
-  with Not_found | Invalid_argument _ ->
-    warn_bytecode_compiler_failed ();
-    gen_conv cv_pb env t1 t2
-
 let default_conv cv_pb ?(l2r=false) env t1 t2 =
     gen_conv cv_pb env t1 t2
 
@@ -880,6 +861,17 @@ let dest_prod env =
   in
   decrec env Context.Rel.empty
 
+let dest_lam env =
+  let rec decrec env m c =
+    let t = whd_all env c in
+    match kind t with
+      | Lambda (n,a,c0) ->
+          let d = LocalAssum (n,a) in
+          decrec (push_rel d env) (Context.Rel.add d m) c0
+      | _ -> m,t
+  in
+  decrec env Context.Rel.empty
+
 (* The same but preserving lets in the context, not internal ones. *)
 let dest_prod_assum env =
   let rec prodec_rec env l ty =
@@ -925,3 +917,12 @@ let is_arity env c =
     let _ = dest_arity env c in
     true
   with NotArity -> false
+
+let eta_expand env t ty =
+  let ctxt, codom = dest_prod env ty in
+  let ctxt',t = dest_lam env t in
+  let d = Context.Rel.nhyps ctxt - Context.Rel.nhyps ctxt' in
+  let eta_args = List.rev_map mkRel (List.interval 1 d) in
+  let t = Term.applistc (Vars.lift d t) eta_args in
+  let t = Term.it_mkLambda_or_LetIn t (List.firstn d ctxt) in
+  Term.it_mkLambda_or_LetIn t ctxt'