Correct rebase on STM code. Thanks to E. Tassi for help on dealing with

latent universes. Now the universes in the type of a definition/lemma
are eagerly added to the environment so that later proofs can be checked
independently of the original (delegated) proof body.

- Fixed firstorder, ring to work correctly with universe polymorphism.
- Changed constr_of_global to raise an anomaly if side effects would be lost by
turning a polymorphic constant into a constr.
- Fix a non-termination issue in solve_evar_evar.
-

1 files changed, 6 insertions, 5 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index d0a477431f..291da4a983 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -26,7 +26,7 @@ open Util
 type proofview = Proofview_monad.proofview
 open Proofview_monad
 
-type entry = (Term.constr * Term.types) list
+type entry = (Term.constr * Term.types Univ.in_universe_context_set) list
 
 let proofview p =
   p.comb , p.solution
@@ -42,7 +42,7 @@ let init sigma =
     let (e, _) = Term.destEvar econstr in
     let new_defs = Evd.merge_context_set Evd.univ_rigid new_defs ctx in
     let gl = Goal.build e in
-    let entry = (econstr, typ) :: ret in
+    let entry = (econstr, (typ, ctx)) :: ret in
     entry, { solution = new_defs; comb = gl::comb; }
   in
   fun l ->
@@ -52,17 +52,18 @@ let init sigma =
 
 type telescope =
   | TNil
-  | TCons of Environ.env*Term.types*(Term.constr -> telescope)
+  | TCons of Environ.env * Term.types Univ.in_universe_context_set * (Term.constr -> telescope)
 
 let dependent_init =
   let rec aux sigma = function
   | TNil -> [], { solution = sigma; comb = []; }
-  | TCons (env, typ, t) ->
+  | TCons (env, (typ, ctx), t) ->
     let (sigma, econstr ) = Evarutil.new_evar sigma env typ in
+    let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in
     let ret, { solution = sol; comb = comb } = aux sigma (t econstr) in
     let (e, _) = Term.destEvar econstr in
     let gl = Goal.build e in
-    let entry = (econstr, typ) :: ret in
+    let entry = (econstr, (typ, ctx)) :: ret in
     entry, { solution = sol; comb = gl :: comb; }
   in
   fun sigma t ->