1 files changed, 16 insertions, 22 deletions
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 066dfc39..93e74af8 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -63,8 +63,8 @@ type atom =
   | Acofixe of t array * t array * int * t
   | Aprod of Name.t * t * (t -> t)
   | Ameta of metavariable * t
-  | Aevar of Evar.t * t * t array
-  | Aproj of Constant.t * accumulator
+  | Aevar of Evar.t * t array
+  | Aproj of (inductive * int) * accumulator
 
 let accumulate_tag = 0
 
@@ -117,7 +117,7 @@ let mk_ind_accu ind u =
 let mk_sort_accu s u =
   let open Sorts in
   match s with
-  | Prop _ -> mk_accu (Asort s)
+  | Prop | Set -> mk_accu (Asort s)
   | Type s ->
      let u = Univ.Instance.of_array u in
      let s = Univ.subst_instance_universe u s in
@@ -135,8 +135,8 @@ let mk_prod_accu s dom codom =
 let mk_meta_accu mv ty =
   mk_accu (Ameta (mv,ty))
 
-let mk_evar_accu ev ty args =
-  mk_accu (Aevar (ev,ty,args))
+let mk_evar_accu ev args =
+  mk_accu (Aevar (ev, args))
 
 let mk_proj_accu kn c = 
   mk_accu (Aproj (kn,c))
@@ -154,10 +154,6 @@ let args_of_accu (k:accumulator) =
   let acc = (get_accu k).acc_arg in
   (Obj.magic (Array.of_list acc) : t array)
 
-let is_accu x =
-  let o = Obj.repr x in
-  Obj.is_block o && Int.equal (Obj.tag o) accumulate_tag
-
 let mk_fix_accu rec_pos pos types bodies =
   mk_accu (Afix(types,bodies,rec_pos, pos))
 
@@ -172,19 +168,17 @@ let upd_cofix (cofix :t) (cofix_fun : t) =
   | _ -> assert false
   
 let force_cofix (cofix : t) = 
-  if is_accu cofix then
-    let accu = (Obj.magic cofix : accumulator) in
-    let atom = atom_of_accu accu in
-    match atom with
-    | Acofix(typ,norm,pos,f) ->
-      let args = args_of_accu accu in
-      let f = Array.fold_right (fun arg f -> f arg) args f in
-      let v = f (Obj.magic ()) in
-      set_atom_of_accu accu (Acofixe(typ,norm,pos,v));
-	v
-    | Acofixe(_,_,_,v) -> v 
-    | _ -> cofix
-  else cofix
+  let accu = (Obj.magic cofix : accumulator) in
+  let atom = atom_of_accu accu in
+  match atom with
+  | Acofix(typ,norm,pos,f) ->
+    let args = args_of_accu accu in
+    let f = Array.fold_right (fun arg f -> f arg) args f in
+    let v = f (Obj.magic ()) in
+    set_atom_of_accu accu (Acofixe(typ,norm,pos,v));
+      v
+  | Acofixe(_,_,_,v) -> v
+  | _ -> cofix
 
 let mk_const tag = Obj.magic tag