From a4a0a47dce78a7d580e172331e7e1ee2881dc689 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 15 Dec 2015 14:10:17 +0100 Subject: Fixing e7f7fc3e058 (wrong chop on contexts). This fixes test-suite. --- pretyping/inductiveops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 82168f9c4..f429c51eb 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -308,7 +308,7 @@ let lift_constructor n cs = { let instantiate_params t params sign = let nnonrecpar = rel_context_nhyps sign - List.length params in (* Adjust the signature if recursively non-uniform parameters are not here *) - let _,sign = List.chop nnonrecpar sign in + let _,sign = context_chop nnonrecpar sign in let _,t = decompose_prod_n_assum (rel_context_length sign) t in let subst = subst_of_rel_context_instance sign params in substl subst t -- cgit v1.2.3