diff options
Diffstat (limited to 'plugins/fourier')
| -rw-r--r-- | plugins/fourier/fourierR.ml | 4 | ||||
| -rw-r--r-- | plugins/fourier/vo.itarget | 2 |
2 files changed, 2 insertions, 4 deletions
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 2af79aec9b..b44307590e 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 diff --git a/plugins/fourier/vo.itarget b/plugins/fourier/vo.itarget deleted file mode 100644 index 87d82dacc5..0000000000 --- a/plugins/fourier/vo.itarget +++ /dev/null @@ -1,2 +0,0 @@ -Fourier_util.vo -Fourier.vo |