From b231bc873a1954f0a81a123fb61159e1fa3cf9b7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 29 Dec 2014 16:37:56 +0100
Subject: Fixing bug #3632 for good.

---
 toplevel/classes.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 3d8264ddcd..697664edc7 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -280,7 +280,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
           let ctx = Evd.universe_context evm in
 	  declare_instance_constant k pri global imps ?hook id 
             poly ctx (Option.get term) termtype
-	else if !refine_instance then begin
+	else if !refine_instance || Option.is_empty term then begin
 	  let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
 	    if Flags.is_program_mode () then
 	      let hook vis gr =
-- 
cgit v1.2.3