From 34bcd562cc9c8e5e6b0f3b79a15b9c55dd98813e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 12 Jul 2017 15:29:10 +0200
Subject: The only abstraction-breaking function in Univ is now
 AUContext.instance.

---
 vernac/himsg.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 86dcb6d4dc..784c6d3387 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -909,7 +909,7 @@ let explain_not_match_error = function
       quote (Printer.safe_pr_lconstr_env env Evd.empty t2)
   | IncompatibleConstraints cst ->
     str " the expected (polymorphic) constraints do not imply " ++
-      let cst = Univ.UContext.constraints (Univ.instantiate_univ_context cst) in
+      let cst = Univ.AUContext.instantiate (Univ.AUContext.instance cst) cst in
       quote (Univ.pr_constraints (Termops.pr_evd_level Evd.empty) cst)
 
 let explain_signature_mismatch l spec why =
-- 
cgit v1.2.3