From 004044b5a377dc36938dc83125cbffb4eae7838c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 1 May 2014 17:44:51 +0200
Subject: Allowing the "Declare Instance" command anywhere. This was
 artificially restricted to module types, although it was nothing more than a
 short hand for Axiom + Existing Instance.

---
 toplevel/classes.ml | 2 --
 1 file changed, 2 deletions(-)

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 6c447e886c..2e17f646bd 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -165,8 +165,6 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
   let subst = List.map (Evarutil.nf_evar sigma) subst in
     if abstract then
       begin
-	if not (Lib.is_modtype ()) then
-	  error "Declare Instance while not in Module Type.";
 	let _, ty_constr = instance_constructor k (List.rev subst) in
 	let termtype =
 	  let t = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
-- 
cgit v1.2.3