diff options
author | 2016-07-07 18:40:28 +0200 | |
---|---|---|
committer | 2016-07-07 18:40:28 +0200 | |
commit | 21be7a5dba2fdfa40fd7b4a3d94610947d202bb7 (patch) | |
tree | 5e22ef0c47a1d9467c0c45c59b0566bea98909ae | |
parent | 11e788c86f1354bd727b2c6c01bc90d431e09188 (diff) | |
parent | 8b890de3642bee1140b238348dd76138b3f1a3dc (diff) |
Merge remote-tracking branch 'github/bug4653' into v8.6
-rw-r--r-- | interp/constrintern.ml | 21 | ||||
-rw-r--r-- | pretyping/pretyping.ml | 17 | ||||
-rw-r--r-- | test-suite/bugs/closed/3690.v | 4 |
3 files changed, 26 insertions, 16 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c0c38a183..438aa2f7c 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -481,9 +481,14 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio let bl' = List.map (fun a -> BDRawDef a) bl' in env, bl' @ bl | LocalRawDef((loc,na as locna),def) -> - let indef = intern env def in + let indef = intern env def in + let term, ty = + match indef with + | GCast (loc, b, Misctypes.CastConv t) -> b, t + | _ -> indef, GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) + in (push_name_env lvar (impls_term_list indef) env locna, - (BDRawDef ((loc,(na,Explicit,Some(indef),GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None)))))::bl) + (BDRawDef ((loc,(na,Explicit,Some(term),ty))))::bl) | LocalPattern (loc,p,ty) -> let tyc = match ty with @@ -2034,11 +2039,13 @@ let interp_rawcontext_evars env evdref k bl = let (env, par, _, impls) = List.fold_left (fun (env,params,n,impls) (na, k, b, t) -> + let t' = + if Option.is_empty b then locate_if_hole (loc_of_glob_constr t) na t + else t + in + let t = understand_tcc_evars env evdref ~expected_type:IsType t' in match b with None -> - let t' = locate_if_hole (loc_of_glob_constr t) na t in - let t = - understand_tcc_evars env evdref ~expected_type:IsType t' in let d = LocalAssum (na,t) in let impls = if k == Implicit then @@ -2048,8 +2055,8 @@ let interp_rawcontext_evars env evdref k bl = in (push_rel d env, d::params, succ n, impls) | Some b -> - let c = understand_judgment_tcc env evdref b in - let d = LocalDef (na, c.uj_val, c.uj_type) in + let c = understand_tcc_evars env evdref ~expected_type:(OfType t) b in + let d = LocalDef (na, c, t) in (push_rel d env, d::params, n, impls)) (env,[],k+1,[]) (List.rev bl) in (env, par), impls diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index c8f61c66b..187eba16b 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -953,14 +953,17 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ | CastConv t | CastVM t | CastNative t -> let k = (match k with CastVM _ -> VMcast | CastNative _ -> NATIVEcast | _ -> DEFAULTcast) in let tj = pretype_type empty_valcon env evdref lvar t in - let tval = nf_evar !evdref tj.utj_val in - let cj = match k with + let tval = evd_comb1 (Evarsolve.refresh_universes + ~onlyalg:true ~status:Evd.univ_flexible (Some false) env) + evdref tj.utj_val in + let tval = nf_evar !evdref tval in + let cj, tval = match k with | VMcast -> let cj = pretype empty_tycon env evdref lvar c in - let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in + let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in if not (occur_existential cty || occur_existential tval) then let (evd,b) = Reductionops.vm_infer_conv env !evdref cty tval in - if b then (evdref := evd; cj) + if b then (evdref := evd; cj, tval) else error_actual_type_loc loc env !evdref cj tval (ConversionFailed (env,cty,tval)) @@ -968,16 +971,16 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ str "unresolved arguments remain.") | NATIVEcast -> let cj = pretype empty_tycon env evdref lvar c in - let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in + let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in begin let (evd,b) = Nativenorm.native_infer_conv env !evdref cty tval in - if b then (evdref := evd; cj) + if b then (evdref := evd; cj, tval) else error_actual_type_loc loc env !evdref cj tval (ConversionFailed (env,cty,tval)) end | _ -> - pretype (mk_tycon tval) env evdref lvar c + pretype (mk_tycon tval) env evdref lvar c, tval in let v = mkCast (cj.uj_val, k, tval) in { uj_val = v; uj_type = tval } diff --git a/test-suite/bugs/closed/3690.v b/test-suite/bugs/closed/3690.v index c24173abf..fd9640b89 100644 --- a/test-suite/bugs/closed/3690.v +++ b/test-suite/bugs/closed/3690.v @@ -47,7 +47,7 @@ Type@{Top.21} -> Type@{Top.23} Top.23 < Top.22 *) *) Fail Check @qux@{Set Set}. -Fail Check @qux@{Set Set Set}. +Check @qux@{Type Type Type Type}. (* [qux] should only need two universes *) -Check @qux@{i j k}. (* Error: The command has not failed!, but I think this is suboptimal *) +Check @qux@{i j k l}. (* Error: The command has not failed!, but I think this is suboptimal *) Fail Check @qux@{i j}. |