From 2d747797c427818cdf85d0a0d701c7c9b0106b82 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 20 Oct 2015 16:12:39 +0200
Subject: Proofview.Goal.sigma returns an indexed evarmap.

---
 plugins/quote/quote.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/quote')

diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 8d60b8ba2..04936cd83 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -228,7 +228,7 @@ let compute_ivs f cs gl =
         let (args3, body3) = decompose_lam body2 in
         let nargs3 = List.length args3 in
         let env = Proofview.Goal.env gl in
-        let sigma = Proofview.Goal.sigma gl in
+        let sigma = Tacmach.New.project gl in
         let is_conv = Reductionops.is_conv env sigma in
           begin match decomp_term body3 with
           | Case(_,p,c,lci) -> (* <p> Case c of c1 ... cn end *)
-- 
cgit v1.2.3