diff options
| -rw-r--r-- | pretyping/cases.ml | 7 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 16 | ||||
| -rw-r--r-- | pretyping/evarutil.mli | 1 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 7 |
4 files changed, 20 insertions, 11 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 7b7ef647d..b1cb40250 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -132,11 +132,6 @@ let build_notdep_pred env sigma indf pred = exception NotInferable of ml_case_error -let rec refresh_types t = match kind_of_term t with - | Sort (Type _) -> new_Type () - | Prod (na,u,v) -> mkProd (na,u,refresh_types v) - | _ -> t - let pred_case_ml_fail env sigma isrec (IndType (indf,realargs)) (i,ft) = let pred = let (ind,params) = indf in @@ -147,7 +142,7 @@ let pred_case_ml_fail env sigma isrec (IndType (indf,realargs)) (i,ft) = let j = snd ind in (* index of inductive *) let nbrec = if isrec then count_rec_arg j recargi else 0 in let nb_arg = List.length (recargs.(i)) + nbrec in - let pred = refresh_types (concl_n env sigma nb_arg ft) in + let pred = Evarutil.refresh_universes (concl_n env sigma nb_arg ft) in if noccur_between 1 nb_arg pred then lift (-nb_arg) pred else diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index d4a341d1b..ea3a4fdb8 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -135,6 +135,18 @@ let judge_of_new_Type () = uj_type = mkSort (Type dummy_univ) } *) +(* This refreshes universes in types; works only for inferred types (i.e. for + types of the form (x1:A1)...(xn:An)B with B a sort or an atom in + head normal form) *) +let refresh_universes t = + let modified = ref false in + let rec refresh t = match kind_of_term t with + | Sort (Type _) -> modified := true; new_Type () + | Prod (na,u,v) -> mkProd (na,u,refresh v) + | _ -> t in + let t' = refresh t in + if !modified then t' else t + (* Declaring any type to be in the sort Type shouldn't be harmful since cumulativity now includes Prop and Set in Type. *) let new_type_var env sigma = @@ -193,6 +205,7 @@ let do_restrict_hyps sigma ev args = let env' = reset_with_named_context sign' env in let instance = make_evar_instance env' in let (sigma',nc) = new_isevar_sign env' sigma evd.evar_concl instance in + let nc = refresh_universes nc in (* needed only if nc is an inferred type *) let sigma'' = Evd.define sigma' ev nc in (sigma'', nc) @@ -237,6 +250,7 @@ let ise_map isevars sp = Evd.map isevars.evars sp (* define the existential of section path sp as the constr body *) let ise_define isevars sp body = + let body = refresh_universes body in (* needed only if an inferred type *) isevars.evars <- Evd.define isevars.evars sp body let is_defined_evar isevars (n,_) = Evd.is_defined isevars.evars n @@ -408,7 +422,7 @@ let head_evar = * hyps of the existential, to do a "pop" for each Rel which is * not an argument of the existential, and a subst1 for each which * is, again, with the corresponding variable. This is done by - * Tradevar.evar_define + * evar_define * * Thus, we take the arguments of the existential which we are about * to assign, and zip them with the identifiers in the hypotheses. diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 66e48664a..7519f51cd 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -71,6 +71,7 @@ val define_evar_as_sort : evar_map -> existential -> evar_map * sorts val new_Type_sort : unit -> sorts val new_Type : unit -> constr val judge_of_new_Type : unit -> unsafe_judgment +val refresh_universes : types -> types type type_constraint = constr option type val_constraint = constr option diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index c2f4b4bde..39071a623 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -112,8 +112,6 @@ let transform_rec loc env sigma (pj,c,lf) indt = let ((constr_in : constr -> Dyn.t), (constr_out : Dyn.t -> constr)) = create "constr" -let ctxt_of_ids cl = cl - let mt_evd = Evd.empty let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t) @@ -342,10 +340,11 @@ let rec pretype tycon env isevars lvar lmeta = function | RLetIn(loc,name,c1,c2) -> let j = pretype empty_tycon env isevars lvar lmeta c1 in - let var = (name,Some j.uj_val,j.uj_type) in + let t = Evarutil.refresh_universes j.uj_type in + let var = (name,Some j.uj_val,t) in let tycon = option_app (lift 1) tycon in let j' = pretype tycon (push_rel var env) isevars lvar lmeta c2 in - { uj_val = mkLetIn (name, j.uj_val, j.uj_type, j'.uj_val) ; + { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ; uj_type = type_app (subst1 j.uj_val) j'.uj_type } | ROldCase (loc,isrec,po,c,lf) -> |