From 875c133ad30890ce3338093b5060cb2dd68c5b52 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 4 Oct 2018 17:00:33 +0200
Subject: Remove FCast from CClosure.fterm.

Just like in the Sixth Sense, it turns out it was dead code all along.
---
 pretyping/inferCumulativity.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

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
-- 
cgit v1.2.3