1 files changed, 8 insertions, 16 deletions
diff --git a/checker/closure.ml b/checker/closure.ml
index 184af0e13..b9ae4daa8 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -135,22 +135,16 @@ let betaiotazeta = mkflags [fBETA;fIOTA;fZETA]
  * instantiations (cbv or lazy) are.
  *)
 
-type 'a tableKey =
-  | ConstKey of 'a
-  | VarKey of Id.t
-  | RelKey of int
-
 type table_key = Constant.t puniverses tableKey
 
+
+let eq_pconstant_key (c,u) (c',u') =
+  eq_constant_key c c' && Univ.Instance.equal u u'
+
 module KeyHash =
 struct
   type t = table_key
-  let equal k1 k2 = match k1, k2 with
-  | ConstKey (c1,u1), ConstKey (c2,u2) -> Constant.UserOrd.equal c1 c2 
-    && Univ.Instance.equal u1 u2
-  | VarKey id1, VarKey id2 -> Id.equal id1 id2
-  | RelKey i1, RelKey i2 -> Int.equal i1 i2
-  | (ConstKey _ | VarKey _ | RelKey _), _ -> false
+  let equal = Names.eq_table_key eq_pconstant_key
 
   open Hashset.Combine
 
@@ -201,8 +195,6 @@ let defined_rels flags env =
 
 let mind_equiv_infos info = mind_equiv info.i_env
 
-let eq_table_key = KeyHash.equal
-
 let create mk_cl flgs env =
   { i_flags = flgs;
     i_repr = mk_cl;
@@ -251,7 +243,7 @@ and fterm =
   | FInd of pinductive
   | FConstruct of pconstructor
   | FApp of fconstr * fconstr array
-  | FProj of projection * fconstr
+  | FProj of Projection.t * fconstr
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
   | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
@@ -281,7 +273,7 @@ let update v1 (no,t) =
 type stack_member =
   | Zapp of fconstr array
   | ZcaseT of case_info * constr * constr array * fconstr subs
-  | Zproj of int * int * projection
+  | Zproj of int * int * Projection.t
   | Zfix of fconstr * stack
   | Zshift of int
   | Zupdate of fconstr
@@ -762,7 +754,7 @@ let rec knr info m stk =
        | (_,args,s) -> (m,args@s))
   | FCoFix _ when red_set info.i_flags fIOTA ->
       (match strip_update_shift_app m stk with
-          (_, args, (((ZcaseT _)::_) as stk')) ->
+          (_, args, (((ZcaseT _|Zproj _)::_) as stk')) ->
             let (fxe,fxbd) = contract_fix_vect m.term in
             knit info fxe fxbd (args@stk')
         | (_,args,s) -> (m,args@s))