From a6757b089e1d268517bcba48a9fe33aa47526de2 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 25 Jan 2019 00:06:32 +0100
Subject: Remove Refine Instance Mode option

---
 vernac/classes.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'vernac/classes.mli')

diff --git a/vernac/classes.mli b/vernac/classes.mli
index e7f90ff306..57bb9ce312 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -48,7 +48,6 @@ val declare_instance_constant :
 val new_instance :
   pstate:Proof_global.t option ->
   ?global:bool (** Not global by default. *) ->
-  ?refine:bool (** Allow refinement *) ->
   program_mode:bool ->
   Decl_kinds.polymorphic ->
   local_binder_expr list ->
-- 
cgit v1.2.3