From 93a77f3cb8ee36072f93b4c0ace6f0f9c19f51a3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Mar 2016 18:41:37 +0100
Subject: Moving Refine to its proper module.

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

(limited to 'toplevel')

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 0a83c49c8d..4bf0450d27 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -330,7 +330,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 		if not (Option.is_empty term) then
                   let init_refine =
                     Tacticals.New.tclTHENLIST [
-                      Proofview.Refine.refine { run = fun evm -> Sigma (Option.get term, evm, Sigma.refl) };
+                      Refine.refine { run = fun evm -> Sigma (Option.get term, evm, Sigma.refl) };
                       Proofview.Unsafe.tclNEWGOALS gls;
                       Tactics.New.reduce_after_refine;
                     ]
-- 
cgit v1.2.3