From 3b980d937b5adfbae472ed8a13748a451fdf3450 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 4 Apr 2019 18:17:57 +0200
Subject: Remove calls to global env from indrec

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

(limited to 'plugins/ssr/ssrequality.ml')

diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 5abbc214de..a7a3fee942 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -340,7 +340,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
   let elim, gl = 
     let ((kn, i) as ind, _), unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in
     let sort = elimination_sort_of_goal gl in
-    let elim, gl = pf_fresh_global (Indrec.lookup_eliminator ind sort) gl in
+    let elim, gl = pf_fresh_global (Indrec.lookup_eliminator env ind sort) gl in
     if dir = R2L then elim, gl else (* taken from Coq's rewrite *)
     let elim, _ = destConst elim in
     let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical elim)) in
-- 
cgit v1.2.3