diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-15 14:10:17 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-15 14:34:08 +0100 |
| commit | a4a0a47dce78a7d580e172331e7e1ee2881dc689 (patch) | |
| tree | 39ef3d49896f38fc040542af6bab3ff7f04eda21 | |
| parent | a582737fc27da2c03c8c57c773fc4854c1e88d7a (diff) | |
Fixing e7f7fc3e058 (wrong chop on contexts). This fixes test-suite.
| -rw-r--r-- | pretyping/inductiveops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |