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, 3 insertions, 8 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 0776988d79..ae16fbebee 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1005,14 +1005,6 @@ let fresh_constructor_instance env evd c =
   with_context_set univ_flexible evd (Universes.fresh_constructor_instance env c)
 
 let fresh_global ?(rigid=univ_flexible) env evd gr =
-  (* match gr with *)
-  (* | ConstructRef c -> let evd, c = fresh_constructor_instance env evd c in  *)
-  (* 			evd, mkConstructU c *)
-  (* | IndRef c -> let evd, c = fresh_inductive_instance env evd c in *)
-  (* 		  evd, mkIndU c *)
-  (* | ConstRef c -> let evd, c = fresh_constant_instance env evd c in *)
-  (* 		    evd, mkConstU c *)
-  (* | VarRef i -> evd, mkVar i *)
   with_context_set rigid evd (Universes.fresh_global_instance env gr)
 
 let whd_sort_variable evd t = t
@@ -1420,6 +1412,9 @@ type 'a sigma = {
 
 let sig_it x = x.it
 let sig_sig x = x.sigma
+let on_sig s f = 
+  let sigma', v = f s.sigma in
+    { s with sigma = sigma' }, v
 
 (*******************************************************************)
 (* The state monad with state an evar map. *)