diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-07-07 17:04:45 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-07-07 17:06:39 +0200 |
| commit | 7c7726a798caa6b506a727703de24d2bb5bb3956 (patch) | |
| tree | e65226bba40098323b59cf8294cf12c1a5bffe82 /kernel/inductive.ml | |
| 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 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 4c1614bac..35b29e73a 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -96,11 +96,11 @@ let full_inductive_instantiate mib u params sign = let ar = fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) in Vars.subst_instance_context u ar -let full_constructor_instantiate ((mind,_),u,(mib,_),params) = - let inst_ind = constructor_instantiate mind u mib in - (fun t -> - instantiate_params true (inst_ind t) params mib.mind_params_ctxt) - +let full_constructor_instantiate ((mind,_),u,(mib,_),params) t = + let inst_ind = constructor_instantiate mind u mib t in + instantiate_params true inst_ind params + (Vars.subst_instance_context u mib.mind_params_ctxt) + (************************************************************************) (************************************************************************) |