From 0d6f26fe444a0a958eda5ac3a1efebca54de40ff Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen 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