From a273df3af0e4315fd792efd83b9365320531111d Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sun, 29 Jun 2014 17:42:13 +0200 Subject: When building on-the-fly elimination principles, set the predicates universe variable as algebraic so it can disappear from the proof (it always gets substituted away from the term). This means less spurious universes remaining in proof terms. --- pretyping/indrec.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'pretyping/indrec.ml') 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) -- cgit v1.2.3