aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-07-10 14:46:56 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-07-10 14:46:56 +0200
commita68c539b6cbe119290df0c6c065cab8ee4746c09 (patch)
tree37b5ff24c2518e335ad9097751844943c40844a6 /pretyping
parentda61ebd063b94eb1f20b5c467457f8b6a21f2707 (diff)
parent107e9dfe3b7a75313029336222e34ecd58cd52a9 (diff)
Merge PR #7983: Turn a dead branch into an assertion failure in VM reification.
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/vnorm.ml2
1 files changed, 1 insertions, 1 deletions
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