diff options
Diffstat (limited to 'plugins/romega/ReflOmegaCore.v')
| -rw-r--r-- | plugins/romega/ReflOmegaCore.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index 51b99b993..f4ac202f2 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -1866,7 +1866,7 @@ Qed. End IntOmega. -(** For now, the above modular construction is instanciated on Z, +(** For now, the above modular construction is instantiated on Z, in order to retrieve the initial ROmega. *) Module ZOmega := IntOmega(Z_as_Int). |