aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/romega
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/romega')
-rw-r--r--plugins/romega/const_omega.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 796b3c7d1..f4368a1bb 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -192,8 +192,8 @@ let rec do_list = function
(* Nat *)
-let coq_S = lazy(constant "S")
-let coq_O = lazy(constant "O")
+let coq_S = lazy(init_constant "S")
+let coq_O = lazy(init_constant "O")
let rec mk_nat = function
| 0 -> Lazy.force coq_O