From 0d6f26fe444a0a958eda5ac3a1efebca54de40ff Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 22 Mar 2004 11:22:03 +0000
Subject: [PATCH] ...
---
helm/ocaml/cic/helmLibraryObjects.ml | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/helm/ocaml/cic/helmLibraryObjects.ml b/helm/ocaml/cic/helmLibraryObjects.ml
index dc621c5a9..b2023b448 100644
--- a/helm/ocaml/cic/helmLibraryObjects.ml
+++ b/helm/ocaml/cic/helmLibraryObjects.ml
@@ -120,6 +120,7 @@ module Reals =
let rgt_URI = uri rgt_SURI
let rtheory_URI = uri "cic:/Coq/Reals/Rbase/RTheory.con"
let rinv_r1_URI = uri "cic:/Coq/Reals/Rbase/Rinv_R1.con"
+ let pow_URI = uri "cic:/Coq/Reals/Rfunctions/pow.con"
let r = const r_URI
let rplus = const rplus_URI
@@ -175,6 +176,8 @@ module BinPos =
module BinInt =
struct
+ let zmult_URI = uri "cic:/Coq/ZArith/BinInt/Zmult.con"
+ let zmult = const zmult_URI
let zplus_SURI = "cic:/Coq/ZArith/BinInt/Zplus.con"
let zplus_URI = uri zplus_SURI
let zplus = const zplus_URI
@@ -189,6 +192,7 @@ module BinInt =
let zopp_SURI = "cic:/Coq/ZArith/BinInt/Zopp.con"
let zopp_URI = uri zopp_SURI
let zopp = const zopp_URI
+ let zpower_URI = uri "cic:/Coq/ZArith/Zpower/Zpower.con"
end
(** {2 Helpers for creating common terms}
--
2.39.2