From 7babf0d42af11f5830bc157a671bd81b478a4f02 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 1 Apr 2017 02:36:16 +0200
Subject: Using delayed universe instances in EConstr.

The transition has been done a bit brutally. I think we can still save a
lot of useless normalizations here and there by providing the right API
in EConstr. Nonetheless, this is a first step.
---
 vernac/classes.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'vernac/classes.ml')

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 415b98f2d8..c3300a3610 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -166,8 +166,9 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
     let imps = imps @ Impargs.lift_implicits len imps' in
     let ctx', c = decompose_prod_assum c' in
     let ctx'' = ctx' @ ctx in
-    let k, args = Typeclasses.dest_class_app (push_rel_context ctx'' env) !evars (EConstr.of_constr c) in
-    let cl, u = Typeclasses.typeclass_univ_instance k in
+    let (k, u), args = Typeclasses.dest_class_app (push_rel_context ctx'' env) !evars (EConstr.of_constr c) in
+    let u = EConstr.EInstance.kind !evars u in
+    let cl, u = Typeclasses.typeclass_univ_instance (k, u) in
     let _, args = 
       List.fold_right (fun decl (args, args') ->
 	match decl with
-- 
cgit v1.2.3