From 107e9dfe3b7a75313029336222e34ecd58cd52a9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 3 Jul 2018 13:38:42 +0200
Subject: Turn a dead branch into an assertion failure in VM reification.

In #7607, dead code that used to handle non-dependent return predicates
was removed. This made the reification branch expecting non-functions
in predicates dead code. We fix this by using an assert instead.
---
 pretyping/vnorm.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 440076c16..c94408050 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -311,7 +311,7 @@ and nf_predicate env sigma ind mip params v pT =
       let dom = mkApp(mkIndU ind,Array.append params rargs) in
       let body = nf_vtype (push_rel (LocalAssum (name,dom)) env) sigma vb in
       mkLambda(name,dom,body)
-    | _ -> nf_val env sigma v crazy_type
+    | _ -> assert false
 
 and nf_args env sigma vargs ?from:(f=0) t =
   let t = ref t in
-- 
cgit v1.2.3