From b098de535db3a17777fb77733229bbbfb914511f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Thu, 21 Jun 2018 10:36:17 +0200
Subject: Fix #5719: Uncaught exception Invalid_argument.

It seems that lifting a term with a negative index is not equivalent to
strengthening it by applying to a dummy substitution. This looks suspicious
at best.
---
 pretyping/cases.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 93ca9dc5e..2d72b9db6 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1699,7 +1699,8 @@ let abstract_tycon ?loc env evdref subst tycon extenv t =
 	let ty = get_type_of env !evdref t in
 	  Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty
       in
-      let ty = lift (-k) (aux x ty) in
+      let dummy_subst = List.init k (fun _ -> mkProp) in
+      let ty = substl dummy_subst (aux x ty) in
       let depvl = free_rels !evdref ty in
       let inst =
 	List.map_i
-- 
cgit v1.2.3