diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-06-29 17:42:13 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-06-29 17:42:13 +0200 |
| commit | a273df3af0e4315fd792efd83b9365320531111d (patch) | |
| tree | 08b521031bfd19ffbe49f50ba3b711e939f09bfb /pretyping/indrec.ml | |
| parent | 85f95cc9f11dc630e59f3a13362e151134ce92ea (diff) | |
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.
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) |