aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/fourier
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-06-12 16:20:15 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-06-12 16:43:33 +0200
commit9097e9a84cf3841cd5fac81a7fe309ae2dec246f (patch)
tree7358a5db6e5f6f17974cc61b4491248f30a332b4 /plugins/fourier
parent013c0232953f1f5832c30940119da05847e99ce2 (diff)
parentb6feaafc7602917a8ef86fb8adc9651ff765e710 (diff)
Merge PR#718: API cleanup: aliases
Diffstat (limited to 'plugins/fourier')
-rw-r--r--plugins/fourier/fourierR.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 2af79aec9..b44307590 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -77,8 +77,8 @@ let flin_emult a f =
type ineq = Rlt | Rle | Rgt | Rge
let string_of_R_constant kn =
- match Names.repr_con kn with
- | MPfile dir, sec_dir, id when
+ match Constant.repr3 kn with
+ | ModPath.MPfile dir, sec_dir, id when
sec_dir = DirPath.empty &&
DirPath.to_string dir = "Coq.Reals.Rdefinitions"
-> Label.to_string id