diff options
| author |  Matej Košík <matej.kosik@inria.fr> | 2017-05-29 11:02:06 +0200 |
|---|---|---|
| committer | Matej Košík <matej.kosik@inria.fr> | 2017-06-10 10:33:53 +0200 |
| commit | b6feaafc7602917a8ef86fb8adc9651ff765e710 (patch) | |
| tree | 5a033488c31040009adb725f20e8bd0a5dd31bc5 /plugins/ssr/ssrequality.ml | |
| parent | 102d7418e399de646b069924277e4baea1badaca (diff) | |
Remove (useless) aliases from the API.
Diffstat (limited to 'plugins/ssr/ssrequality.ml')
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index dbe13aec9..b0fe89897 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 |