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 | |
| 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.
| -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) |