From b6feaafc7602917a8ef86fb8adc9651ff765e710 Mon Sep 17 00:00:00 2001
From: Matej Košík
Date: Mon, 29 May 2017 11:02:06 +0200
Subject: Remove (useless) aliases from the API.

---
 plugins/ssr/ssrequality.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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

diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index dbe13aec9f..b0fe898975 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -343,9 +343,9 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
     let elim, gl = pf_fresh_global (Indrec.lookup_eliminator ind sort) gl in
     if dir = R2L then elim, gl else (* taken from Coq's rewrite *)
     let elim, _ = Term.destConst elim in          
-    let mp,dp,l = repr_con (constant_of_kn (canonical_con elim)) in
+    let mp,dp,l = Constant.repr3 (Constant.make1 (Constant.canonical elim)) in
     let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r")  in 
-    let c1' = Global.constant_of_delta_kn (canonical_con (make_con mp dp l')) in
+    let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make3 mp dp l')) in
     mkConst c1', gl in
   let elim = EConstr.of_constr elim in
   let proof = EConstr.mkApp (elim, [| rdx_ty; new_rdx; pred; p; rdx; c |]) in
-- 
cgit v1.2.3