diff options
| author |  Matej Košík <matej.kosik@inria.fr> | 2017-06-07 14:25:07 +0200 |
|---|---|---|
| committer | Matej Košík <matej.kosik@inria.fr> | 2017-06-07 14:49:13 +0200 |
| commit | 34dd34065111c5abe68e88a79a77e482e79489a7 (patch) | |
| tree | 624eb098d442a5b30e55729404830b8fe7bac0bb /plugins/ssr/ssrequality.ml | |
| parent | 661940fd55a925a6f17f6025f5d15fc9f5647cf9 (diff) | |
Put "ssreflect" behind "API".
Diffstat (limited to 'plugins/ssr/ssrequality.ml')
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index af315aac5..dbe13aec9 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 @@ -343,7 +344,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = 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 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 mkConst c1', gl in let elim = EConstr.of_constr elim in |