1 files changed, 34 insertions, 62 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 2ae676bc..c701b53f 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -53,7 +53,7 @@ let compare_stack_shape stk1 stk2 =
     | (_, (Zupdate _|Zshift _)::s2) -> compare_rec bal stk1 s2
     | (Zapp l1::s1, _) -> compare_rec (bal+Array.length l1) s1 stk2
     | (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2
-    | (Zproj (n1,m1,p1)::s1, Zproj (n2,m2,p2)::s2) ->
+    | (Zproj p1::s1, Zproj p2::s2) ->
         Int.equal bal 0 && compare_rec 0 s1 s2
     | (ZcaseT(c1,_,_,_)::s1, ZcaseT(c2,_,_,_)::s2) ->
         Int.equal bal 0 (* && c1.ci_ind  = c2.ci_ind *) && compare_rec 0 s1 s2
@@ -66,7 +66,7 @@ let compare_stack_shape stk1 stk2 =
 
 type lft_constr_stack_elt =
     Zlapp of (lift * fconstr) array
-  | Zlproj of Constant.t * lift
+  | Zlproj of Projection.Repr.t * lift
   | Zlfix of (lift * fconstr) * lft_constr_stack
   | Zlcase of case_info * lift * fconstr * fconstr array
 and lft_constr_stack = lft_constr_stack_elt list
@@ -84,7 +84,7 @@ let map_lift (l : lift) (v : fconstr array) = match v with
 | [|c0; c1|] -> [|(l, c0); (l, c1)|]
 | [|c0; c1; c2|] -> [|(l, c0); (l, c1); (l, c2)|]
 | [|c0; c1; c2; c3|] -> [|(l, c0); (l, c1); (l, c2); (l, c3)|]
-| v -> CArray.Fun1.map (fun l t -> (l, t)) l v
+| v -> Array.Fun1.map (fun l t -> (l, t)) l v
 
 let pure_stack lfts stk =
   let rec pure_rec lfts stk =
@@ -96,8 +96,8 @@ let pure_stack lfts stk =
             | (Zshift n,(l,pstk)) -> (el_shft n l, pstk)
             | (Zapp a, (l,pstk)) ->
                 (l,zlapp (map_lift l a) pstk)
-	    | (Zproj (n,m,c), (l,pstk)) ->
-		(l, Zlproj (c,l)::pstk)
+            | (Zproj p, (l,pstk)) ->
+                (l, Zlproj (p,l)::pstk)
             | (Zfix(fx,a),(l,pstk)) ->
                 let (lfx,pa) = pure_rec l a in
                 (l, Zlfix((lfx,fx),pa)::pstk)
@@ -297,7 +297,7 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv =
             | (Zlapp a1,Zlapp a2) -> 
 	       Array.fold_right2 f a1 a2 cu1
 	    | (Zlproj (c1,l1),Zlproj (c2,l2)) -> 
-	      if not (Constant.equal c1 c2) then 
+              if not (Projection.Repr.equal c1 c2) then
 		raise NotConvertible
 	      else cu1
             | (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
@@ -408,7 +408,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         | Some s2 ->
           eqappr cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv
 	| None -> 
-          if Constant.equal (Projection.constant p1) (Projection.constant p2)
+          if Projection.Repr.equal (Projection.repr p1) (Projection.repr p2)
 	     && compare_stack_shape v1 v2 then
             let el1 = el_stack lft1 v1 in
             let el2 = el_stack lft2 v2 in
@@ -649,23 +649,19 @@ let check_leq univs u u' =
 let check_sort_cmp_universes env pb s0 s1 univs =
   let open Sorts in
   if not (type_in_type env) then
+    let check_pb u0 u1 =
+      match pb with
+      | CUMUL -> check_leq univs u0 u1
+      | CONV -> check_eq univs u0 u1
+    in
     match (s0,s1) with
-    | (Prop c1, Prop c2) when is_cumul pb ->
-      begin match c1, c2 with
-        | Null, _ | _, Pos -> () (* Prop <= Set *)
-        | _ -> raise NotConvertible
-      end
-    | (Prop c1, Prop c2) -> if c1 != c2 then raise NotConvertible
-    | (Prop c1, Type 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) ->
-      (match pb with
-       | CUMUL -> check_leq univs u1 u2
-       | CONV -> check_eq univs u1 u2)
+    | Prop, Prop | Set, Set -> ()
+    | Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible
+    | Set, Prop -> raise NotConvertible
+    | Set, Type u -> check_pb Univ.type0_univ u
+    | Type u, Prop -> raise NotConvertible
+    | Type u, Set -> check_pb u Univ.type0_univ
+    | Type u0, Type u1 -> check_pb u0 u1
 
 let checked_sort_cmp_universes env pb s0 s1 univs =
   check_sort_cmp_universes env pb s0 s1 univs; univs
@@ -697,26 +693,23 @@ let infer_leq (univs, cstrs as cuniv) u u' =
       univs, Univ.Constraint.union cstrs cstrs'
 
 let infer_cmp_universes env pb s0 s1 univs =
-  let open Sorts in
-  if type_in_type env then univs
+  if type_in_type env
+  then univs
   else
+    let open Sorts in
+    let infer_pb u0 u1 =
+      match pb with
+      | CUMUL -> infer_leq univs u0 u1
+      | CONV -> infer_eq univs u0 u1
+    in
     match (s0,s1) with
-    | (Prop c1, Prop c2) when is_cumul pb ->
-      begin match c1, c2 with
-        | 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)
-    | (Type u, Prop c) -> raise NotConvertible
-    | (Type u1, Type u2) ->
-      (match pb with
-       | CUMUL -> infer_leq univs u1 u2
-       | CONV -> infer_eq univs u1 u2)
+    | Prop, Prop | Set, Set -> univs
+    | Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible else univs
+    | Set, Prop -> raise NotConvertible
+    | Set, Type u -> infer_pb Univ.type0_univ u
+    | Type u, Prop -> raise NotConvertible
+    | Type u, Set -> infer_pb u Univ.type0_univ
+    | Type u0, Type u1 -> infer_pb u0 u1
 
 let infer_convert_instances ~flex u u' (univs,cstrs) =
   let cstrs' =
@@ -788,24 +781,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
 
@@ -937,7 +912,6 @@ let is_arity env c =
   with NotArity -> false
 
 let eta_expand env t ty =
-  let env = env_of_pre_env env in
   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
@@ -945,5 +919,3 @@ let eta_expand env t ty =
   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'
-
-let _ = Hook.set Clambda.eta_expand_hook eta_expand