diff options
Diffstat (limited to 'pretyping/indrec.ml')
| -rw-r--r-- | pretyping/indrec.ml | 7 |
1 files changed, 5 insertions, 2 deletions
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) |