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, 2 insertions, 1 deletions

diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 563148872..9ae8fcbf6 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -78,7 +78,8 @@ let gen_ground_tac flag taco ids bases gl=
 	  | None-> snd (default_solver ()) in
       let startseq gl=
 	let seq=empty_seq !ground_depth in
-	extend_with_auto_hints bases (extend_with_ref_list ids seq gl) gl in
+        let seq,gl = extend_with_ref_list ids seq gl in
+        extend_with_auto_hints bases seq gl in
       let result=ground_tac (Proofview.V82.of_tactic solver) startseq gl in
 	qflag:=backup;result
     with reraise -> qflag:=backup;raise reraise