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/evd.ml    | 4 ++--
 pretyping/evd.mli   | 2 +-
 pretyping/indrec.ml | 7 +++++--
 3 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 902ec9f154..481e4275a6 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 b6db3c2636..a44a67656b 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 9f58b4c80d..dba151014c 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