From 83f321c19cfd97e386d7bd5f0aca24ea46c43d2b Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 31 Mar 2017 13:53:08 +0200
Subject: Instances should obey universe binders even when defined by tactics.

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

(limited to 'toplevel/classes.ml')

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 1528cbb2f6..8142d48d88 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -332,7 +332,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
                      the refinement manually.*)
 		let gls = List.rev (Evd.future_goals evm) in
                 let evm = Evd.reset_future_goals evm in
-                Lemmas.start_proof id kind evm termtype
+                Lemmas.start_proof id ?pl kind evm termtype
 		(Lemmas.mk_hook
                   (fun _ -> instance_hook k pri global imps ?hook));
                  (* spiwack: I don't know what to do with the status here. *)
-- 
cgit v1.2.3