diff options
| author | Matthieu Sozeau | 2015-07-07 17:04:45 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-07-07 17:06:39 +0200 |
| commit | 7c7726a798caa6b506a727703de24d2bb5bb3956 (patch) | |
| tree | e65226bba40098323b59cf8294cf12c1a5bffe82 /pretyping | |
| parent | 024a7ab20b06d82571c68c3d2ac32cb60fb0053a (diff) | |
Univs: bug fix.
Missing universe substitutions of mind_params_ctxt when typechecking
cases, which appeared only when let-ins were used.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/inductiveops.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 90aa8000a8..cb091f2d6f 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -322,7 +322,8 @@ let instantiate_params t args sign = let get_constructor ((ind,u as indu),mib,mip,params) j = assert (j <= Array.length mip.mind_consnames); let typi = mis_nf_constructor_type (indu,mib,mip) j in - let typi = instantiate_params typi params mib.mind_params_ctxt in + let ctx = Vars.subst_instance_context u mib.mind_params_ctxt in + let typi = instantiate_params typi params ctx in let (args,ccl) = decompose_prod_assum typi in let (_,allargs) = decompose_app ccl in let vargs = List.skipn (List.length params) allargs in |