From f16290030b48dedf3091334af4cd21a7df157381 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 30 Sep 2020 13:21:02 +0200
Subject: Further simplification of the typeclass registration API.

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

(limited to 'plugins')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index a1dbf9a439..8de6cbc0a6 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -181,7 +181,7 @@ end) = struct
     fun env sigma -> class_info env sigma (Lazy.force r)
 
   let proper_proj env sigma =
-    mkConst (Option.get (pi3 (List.hd (proper_class env sigma).cl_projs)))
+    mkConst (Option.get (List.hd (proper_class env sigma).cl_projs).meth_const)
 
   let proper_type env (sigma,cstrs) =
     let l = (proper_class env sigma).cl_impl in
-- 
cgit v1.2.3