Remove FCast from CClosure.fterm.

Just like in the Sixth Sense, it turns out it was dead code all along.

4 files changed, 5 insertions, 10 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 003b49535f..819a66c190 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -359,7 +359,6 @@ type fconstr = {
 and fterm =
   | FRel of int
   | FAtom of constr (* Metas and Sorts *)
-  | FCast of fconstr * cast_kind * fconstr
   | FFlex of table_key
   | FInd of pinductive
   | FConstruct of pconstructor
@@ -477,7 +476,7 @@ let rec lft_fconstr n ft =
     | FCoFix(cfx,e) -> {norm=Cstr; term=FCoFix(cfx,subs_shft(n,e))}
     | FLIFT(k,m) -> lft_fconstr (n+k) m
     | FLOCKED -> assert false
-    | FFlex _ | FAtom _ | FCast _ | FApp _ | FProj _ | FCaseT _ | FProd _
+    | FFlex _ | FAtom _ | FApp _ | FProj _ | FCaseT _ | FProd _
       | FLetIn _ | FEvar _ | FCLOS _ -> {norm=ft.norm; term=FLIFT(n,ft)}
 let lift_fconstr k f =
   if Int.equal k 0 then f else lft_fconstr k f
@@ -558,8 +557,6 @@ let rec to_constr lfts v =
     | FFlex (RelKey p) -> mkRel (reloc_rel p lfts)
     | FFlex (VarKey x) -> mkVar x
     | FAtom c -> exliftn lfts c
-    | FCast (a,k,b) ->
-      mkCast (to_constr lfts a, k, to_constr lfts b)
     | FFlex (ConstKey op) -> mkConstU op
     | FInd op -> mkIndU op
     | FConstruct op -> mkConstructU op
@@ -866,7 +863,6 @@ let rec knh info m stk =
         (match get_nth_arg m ri.(n) stk with
              (Some(pars,arg),stk') -> knh info arg (Zfix(m,pars)::stk')
            | (None, stk') -> (m,stk'))
-    | FCast(t,_,_) -> knh info t stk
     | FProj (p,c) ->
       (match unfold_projection info p with
        | None -> (m, stk)
@@ -951,7 +947,7 @@ let rec knr info tab m stk =
       (match evar_value info.i_cache ev with
           Some c -> knit info tab env c stk
         | None -> (m,stk))
-  | FLOCKED | FRel _ | FAtom _ | FCast _ | FFlex _ | FInd _ | FApp _ | FProj _
+  | FLOCKED | FRel _ | FAtom _ | FFlex _ | FInd _ | FApp _ | FProj _
     | FFix _ | FCoFix _ | FCaseT _ | FLambda _ | FProd _ | FLetIn _ | FLIFT _
     | FCLOS _ -> (m, stk)
 
@@ -1031,7 +1027,7 @@ and norm_head info tab m =
           mkEvar(i, Array.map (fun a -> kl info tab (mk_clos env a)) args)
       | FProj (p,c) ->
           mkProj (p, kl info tab c)
-      | FLOCKED | FRel _ | FAtom _ | FCast _ | FFlex _ | FInd _ | FConstruct _
+      | FLOCKED | FRel _ | FAtom _ | FFlex _ | FInd _ | FConstruct _
         | FApp _ | FCaseT _ | FLIFT _ | FCLOS _ -> term_of_fconstr m
 
 (* Initialization and then normalization *)
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 6121b3a1ec..2a018d172a 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -131,7 +131,6 @@ type fconstr
 type fterm =
   | FRel of int
   | FAtom of constr (** Metas and Sorts *)
-  | FCast of fconstr * cast_kind * fconstr
   | FFlex of table_key
   | FInd of inductive Univ.puniverses
   | FConstruct of constructor Univ.puniverses
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 2abb4b485c..00576476ab 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -605,7 +605,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
      (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *)
      | ( (FLetIn _, _) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_)
        | (_, FLetIn _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _)
-       | (FLOCKED,_) | (_,FLOCKED) ) | (FCast _, _) | (_, FCast _) -> assert false
+       | (FLOCKED,_) | (_,FLOCKED) ) -> assert false
 
      | (FRel _ | FAtom _ | FInd _ | FFix _ | FCoFix _
         | FProd _ | FEvar _), _ -> raise NotConvertible
diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml
index be79b8b07d..a56a8314e6 100644
--- a/pretyping/inferCumulativity.ml
+++ b/pretyping/inferCumulativity.ml
@@ -137,7 +137,7 @@ let rec infer_fterm cv_pb infos variances hd stk =
     infer_stack infos variances stk
 
   (* Removed by whnf *)
-  | FLOCKED | FCaseT _ | FCast _ | FLetIn _ | FApp _ | FLIFT _ | FCLOS _ -> assert false
+  | FLOCKED | FCaseT _ | FLetIn _ | FApp _ | FLIFT _ | FCLOS _ -> assert false
 
 and infer_stack infos variances (stk:CClosure.stack) =
   match stk with