When defining a monomorphic Program, do not allow arbitrary instantiations

of the universe context in the obligations, it gets gradually fixed
globally by each one of them.
Fixes bug found in Misc/Overloading.

1 files changed, 7 insertions, 0 deletions

diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index fc1df9f00d..8f637aa325 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -833,6 +833,13 @@ let rec solve_obligation prg num tac =
 		in
 		let obls = Array.copy obls in
 		let _ = obls.(num) <- obl in
+		let ctx' = 
+		  if not (pi2 prg.prg_kind) (* Not polymorphic *) then
+		    (* This context is already declared globally, we cannot 
+		       instantiate the rigid variables anymore *) 
+		    Evd.abstract_undefined_variables ctx'
+		  else ctx'
+		in
 		let res = 
 		  try update_obls 
 			{prg with prg_body = prg.prg_body;