diff options
| -rw-r--r-- | pretyping/evd.ml | 4 | ||||
| -rw-r--r-- | pretyping/evd.mli | 2 | ||||
| -rw-r--r-- | pretyping/indrec.ml | 7 |
3 files changed, 8 insertions, 5 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 902ec9f15..481e4275a 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1035,8 +1035,8 @@ let make_flexible_variable evd b u = (* Operations on constants *) (****************************************) -let fresh_sort_in_family env evd s = - with_context_set univ_flexible evd (Universes.fresh_sort_in_family env s) +let fresh_sort_in_family ?(rigid=univ_flexible) env evd s = + with_context_set rigid evd (Universes.fresh_sort_in_family env s) let fresh_constant_instance env evd c = with_context_set univ_flexible evd (Universes.fresh_constant_instance env c) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index b6db3c263..a44a67656 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -486,7 +486,7 @@ val nf_constraints : evar_map -> evar_map (** Polymorphic universes *) -val fresh_sort_in_family : env -> evar_map -> sorts_family -> evar_map * sorts +val fresh_sort_in_family : ?rigid:rigid -> env -> evar_map -> sorts_family -> evar_map * sorts val fresh_constant_instance : env -> evar_map -> constant -> evar_map * pconstant val fresh_inductive_instance : env -> evar_map -> inductive -> evar_map * pinductive val fresh_constructor_instance : env -> evar_map -> constructor -> evar_map * pconstructor diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 9f58b4c80..dba151014 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -111,7 +111,7 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = mkLambda_string "f" t (add_branch (push_rel (Anonymous, None, t) env) (k+1)) in - let sigma, s = Evd.fresh_sort_in_family env sigma kind in + let sigma, s = Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env sigma kind in let typP = make_arity env' dep indf s in let c = it_mkLambda_or_LetIn_name env @@ -427,7 +427,10 @@ let mis_make_indrec env sigma listdepkind mib u = let rec put_arity env i = function | ((indi,u),_,_,dep,kinds)::rest -> let indf = make_ind_family ((indi,u), Termops.extended_rel_list i lnamesparrec) in - let s = Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evdref kinds in + let s = + Evarutil.evd_comb1 (Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env) + evdref kinds + in let typP = make_arity env dep indf s in mkLambda_string "P" typP (put_arity (push_rel (Anonymous,None,typP) env) (i+1) rest) |