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.
---
 plugins/quote/quote.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'plugins/quote')

diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 23069a9abc..fc9d70ae7d 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -225,8 +225,9 @@ let compute_rhs env sigma bodyi index_of_f =
 let compute_ivs f cs gl =
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
-  let cst = try destConst sigma f with DestKO -> i_can't_do_that () in
-  let body = Environ.constant_value_in (Global.env()) cst in
+  let (cst, u) = try destConst sigma f with DestKO -> i_can't_do_that () in
+  let u = EInstance.kind sigma u in
+  let body = Environ.constant_value_in (Global.env()) (cst, u) in
   let body = EConstr.of_constr body in
   match decomp_term sigma body with
     | Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) ->
-- 
cgit v1.2.3