From f0196d4e96bf8cc579d1690fc6a653adc08ca02e Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 12 Jan 2004 17:12:39 +0000
Subject: [PATCH] added HelmLibraryObjects module

---
 helm/ocaml/cic/.depend               |  2 ++
 helm/ocaml/cic/Makefile              |  2 +-
 helm/ocaml/cic/helmLibraryObjects.ml | 54 ++++++++++++++++++++++++++++
 3 files changed, 57 insertions(+), 1 deletion(-)
 create mode 100644 helm/ocaml/cic/helmLibraryObjects.ml

diff --git a/helm/ocaml/cic/.depend b/helm/ocaml/cic/.depend
index 591cea8df..3bf9bfede 100644
--- a/helm/ocaml/cic/.depend
+++ b/helm/ocaml/cic/.depend
@@ -10,3 +10,5 @@ cicParser2.cmo: cic.cmo cicParser3.cmi cicParser2.cmi
 cicParser2.cmx: cic.cmx cicParser3.cmx cicParser2.cmi 
 cicParser.cmo: cicParser2.cmi cicParser3.cmi deannotate.cmi cicParser.cmi 
 cicParser.cmx: cicParser2.cmx cicParser3.cmx deannotate.cmx cicParser.cmi 
+helmLibraryObjects.cmo: cic.cmo 
+helmLibraryObjects.cmx: cic.cmx 
diff --git a/helm/ocaml/cic/Makefile b/helm/ocaml/cic/Makefile
index c18667dc2..1789cd67e 100644
--- a/helm/ocaml/cic/Makefile
+++ b/helm/ocaml/cic/Makefile
@@ -3,7 +3,7 @@ REQUIRES = helm-urimanager helm-pxp
 PREDICATES =
 
 INTERFACE_FILES = deannotate.mli cicParser3.mli cicParser2.mli cicParser.mli
-IMPLEMENTATION_FILES = cic.ml $(INTERFACE_FILES:%.mli=%.ml)
+IMPLEMENTATION_FILES = cic.ml $(INTERFACE_FILES:%.mli=%.ml) helmLibraryObjects.ml
 EXTRA_OBJECTS_TO_INSTALL = cic.ml cic.cmi
 EXTRA_OBJECTS_TO_CLEAN =
 
diff --git a/helm/ocaml/cic/helmLibraryObjects.ml b/helm/ocaml/cic/helmLibraryObjects.ml
new file mode 100644
index 000000000..2d4938181
--- /dev/null
+++ b/helm/ocaml/cic/helmLibraryObjects.ml
@@ -0,0 +1,54 @@
+
+let uri = UriManager.uri_of_string
+
+let const ?(subst = []) uri = Cic.Const (uri, subst)
+let var ?(subst = []) uri = Cic.Var (uri, subst)
+let mutconstruct ?(subst = []) uri typeno consno =
+  Cic.MutConstruct (uri, typeno, consno, subst)
+
+module Logic =
+  struct
+    let eq_URI = uri "cic:/Coq/Init/Logic/eq.ind"
+    let true_URI = uri "cic:/Coq/Init/Logic/True.ind"
+    let false_URI = uri "cic:/Coq/Init/Logic/False.ind"
+  end
+
+module Logic_Type =
+  struct
+    let eqt_URI = uri "cic:/Coq/Init/Logic_Type/eqT.ind"
+    let sym_eqt_URI = uri "cic:/Coq/Init/Logic_Type/sym_eqT.con"
+
+    let refl_eqt = mutconstruct eqt_URI 0 1
+    let sym_eqt = const sym_eqt_URI
+  end
+
+module Datatypes =
+  struct
+    let bool_URI = uri "cic:/Coq/Init/Datatypes/bool.ind"
+    let nat_URI = uri "cic:/Coq/Init/Datatypes/nat.ind"
+
+    let trueb = mutconstruct bool_URI 0 1
+    let falseb = mutconstruct bool_URI 0 2
+    let zero = mutconstruct nat_URI 0 1
+    let succ = mutconstruct nat_URI 0 2
+  end
+
+module Reals =
+  struct
+    let r_URI = uri "cic:/Coq/Reals/Rdefinitions/R.con"
+    let rplus_URI = uri "cic:/Coq/Reals/Rdefinitions/Rplus.con"
+    let rmult_URI = uri "cic:/Coq/Reals/Rdefinitions/Rmult.con"
+    let ropp_URI = uri "cic:/Coq/Reals/Rdefinitions/Ropp.con"
+    let r0_URI = uri "cic:/Coq/Reals/Rdefinitions/R0.con"
+    let r1_URI = uri "cic:/Coq/Reals/Rdefinitions/R1.con"
+    let rtheory_URI = uri "cic:/Coq/Reals/Rbase/RTheory.con"
+
+    let r = const r_URI
+    let rplus = const rplus_URI
+    let rmult = const rmult_URI
+    let ropp = const ropp_URI
+    let r0 = const r0_URI
+    let r1 = const r1_URI
+    let rtheory = const rtheory_URI
+  end
+
-- 
2.39.2