diff options
Diffstat (limited to 'plugins/ssr/ssrequality.ml')
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index af315aac5..b0fe89897 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Ltac_plugin open Util open Names @@ -342,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 l' = label_of_id (Nameops.add_suffix (id_of_label l) "_r") in - let c1' = Global.constant_of_delta_kn (canonical_con (make_con mp dp l')) 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 (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 |