diff options
| -rw-r--r-- | pretyping/pretyping.ml | 7 | ||||
| -rw-r--r-- | test-suite/bugs/closed/1951.v | 10 |
2 files changed, 10 insertions, 7 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 2c16c2eb3..27abdbade 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -590,10 +590,13 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t = match evar_kind_of_term !evdref resj.uj_val with | App (f,args) -> let f = whd_evar !evdref f in - if is_template_polymorphic env f then + if isInd f && is_template_polymorphic env f then + (* Special case for inductive type applications that must be + refreshed right away. *) let sigma = !evdref in let c = mkApp (f,Array.map (whd_evar sigma) args) in - let t = Retyping.get_type_of env sigma c in + let c = evd_comb1 (Evarsolve.refresh_universes true env) evdref c in + let t = Retyping.get_type_of env !evdref c in make_judge c (* use this for keeping evars: resj.uj_val *) t else resj | _ -> resj diff --git a/test-suite/bugs/closed/1951.v b/test-suite/bugs/closed/1951.v index 12c0ef9bf..7558b0b86 100644 --- a/test-suite/bugs/closed/1951.v +++ b/test-suite/bugs/closed/1951.v @@ -5,11 +5,11 @@ Set Printing Universes. Inductive enc (A:Type (*1*)) (* : Type.1 *) := C : A -> enc A. -Definition id (X:Type(*5*)) (x:X) := x. +Definition id (X:Type(*4*)) (x:X) := x. -Lemma test : let S := Type(*6 : 7*) in enc S -> S. +Lemma test : let S := Type(*5 : 6*) in enc S -> S. simpl; intros. -apply enc. +refine (enc _). apply id. apply Prop. Defined. @@ -26,7 +26,7 @@ b : (list a) -> a. (* i don't know if this *) Inductive sg : Type := Sg. (* single *) Definition ipl2 (P : a -> Type) := (* in Prop, that means P is true forall *) -fold_right (fun x => prod (P x)) sg. (* the elements of a given list *) + fold_right (fun x => fun A => prod (P x) A) sg. (* the elements of a given list *) Definition ind : forall S : a -> Type, @@ -55,7 +55,7 @@ Defined. Lemma k' : a -> Type. (* same lemma but with our bug *) intro;pattern H;apply ind;intros. - apply prod. + refine (prod _ _). induction ls. exact sg. exact sg. |