diff options
| -rw-r--r-- | kernel/inductive.ml | 10 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 3 | ||||
| -rw-r--r-- | test-suite/success/polymorphism.v | 12 |
3 files changed, 19 insertions, 6 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) + (************************************************************************) (************************************************************************) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 90aa8000a..cb091f2d6 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 diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index dc22b03f2..957612ef1 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -308,3 +308,15 @@ Definition RLRL' : forall x : R, RL x = RL (RL x). Qed. End eta. + +Module Hurkens'. + Require Import Hurkens. + +Polymorphic Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }. + +Definition unwrap' := fun (X : Type) (b : box X) => let (unw) := b in unw. + +Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _ +Type)) eq_refl. + +End Hurkens'.
\ No newline at end of file |