From 264523336352a5241b747b7e04b33630f6010aeb Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 20 Jul 2003 13:08:25 +0000
Subject: [PATCH] Content2cic e Eta_fixing moved from gTopLevel to cic_omdoc.

---
 helm/gTopLevel/.depend                             | 14 ++++----------
 helm/ocaml/cic_omdoc/.depend                       |  5 +++++
 helm/ocaml/cic_omdoc/Makefile                      |  4 ++--
 helm/{gTopLevel => ocaml/cic_omdoc}/content2cic.ml |  0
 .../{gTopLevel => ocaml/cic_omdoc}/content2cic.mli |  0
 helm/{gTopLevel => ocaml/cic_omdoc}/eta_fixing.ml  |  0
 helm/{gTopLevel => ocaml/cic_omdoc}/eta_fixing.mli |  0
 7 files changed, 11 insertions(+), 12 deletions(-)
 rename helm/{gTopLevel => ocaml/cic_omdoc}/content2cic.ml (100%)
 rename helm/{gTopLevel => ocaml/cic_omdoc}/content2cic.mli (100%)
 rename helm/{gTopLevel => ocaml/cic_omdoc}/eta_fixing.ml (100%)
 rename helm/{gTopLevel => ocaml/cic_omdoc}/eta_fixing.mli (100%)

diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend
index e6194df96..d629a155e 100644
--- a/helm/gTopLevel/.depend
+++ b/helm/gTopLevel/.depend
@@ -1,9 +1,5 @@
 proofEngine.cmo: proofEngine.cmi 
 proofEngine.cmx: proofEngine.cmi 
-eta_fixing.cmo: eta_fixing.cmi 
-eta_fixing.cmx: eta_fixing.cmi 
-content2cic.cmo: content2cic.cmi 
-content2cic.cmx: content2cic.cmi 
 logicalOperations.cmo: proofEngine.cmi logicalOperations.cmi 
 logicalOperations.cmx: proofEngine.cmx logicalOperations.cmi 
 disambiguate.cmo: disambiguate.cmi 
@@ -24,9 +20,7 @@ invokeTactics.cmi: termEditor.cmi termViewer.cmi
 hbugs.cmo: invokeTactics.cmi proofEngine.cmi hbugs.cmi 
 hbugs.cmx: invokeTactics.cmx proofEngine.cmx hbugs.cmi 
 hbugs.cmi: invokeTactics.cmi 
-gTopLevel.cmo: eta_fixing.cmi hbugs.cmi invokeTactics.cmi \
-    logicalOperations.cmi proofEngine.cmi termEditor.cmi termViewer.cmi \
-    texTermEditor.cmi 
-gTopLevel.cmx: eta_fixing.cmx hbugs.cmx invokeTactics.cmx \
-    logicalOperations.cmx proofEngine.cmx termEditor.cmx termViewer.cmx \
-    texTermEditor.cmx 
+gTopLevel.cmo: hbugs.cmi invokeTactics.cmi logicalOperations.cmi \
+    proofEngine.cmi termEditor.cmi termViewer.cmi texTermEditor.cmi 
+gTopLevel.cmx: hbugs.cmx invokeTactics.cmx logicalOperations.cmx \
+    proofEngine.cmx termEditor.cmx termViewer.cmx texTermEditor.cmx 
diff --git a/helm/ocaml/cic_omdoc/.depend b/helm/ocaml/cic_omdoc/.depend
index 1ec905424..d12896d47 100644
--- a/helm/ocaml/cic_omdoc/.depend
+++ b/helm/ocaml/cic_omdoc/.depend
@@ -1,4 +1,7 @@
 contentPp.cmi: content.cmi 
+content2cic.cmi: content.cmi 
+eta_fixing.cmo: eta_fixing.cmi 
+eta_fixing.cmx: eta_fixing.cmi 
 doubleTypeInference.cmo: doubleTypeInference.cmi 
 doubleTypeInference.cmx: doubleTypeInference.cmi 
 cic2acic.cmo: doubleTypeInference.cmi cic2acic.cmi 
@@ -7,3 +10,5 @@ content.cmo: content.cmi
 content.cmx: content.cmi 
 contentPp.cmo: content.cmi contentPp.cmi 
 contentPp.cmx: content.cmx contentPp.cmi 
+content2cic.cmo: content.cmi content2cic.cmi 
+content2cic.cmx: content.cmx content2cic.cmi 
diff --git a/helm/ocaml/cic_omdoc/Makefile b/helm/ocaml/cic_omdoc/Makefile
index 0fbb566ae..e1e081ac6 100644
--- a/helm/ocaml/cic_omdoc/Makefile
+++ b/helm/ocaml/cic_omdoc/Makefile
@@ -2,8 +2,8 @@ PACKAGE = cic_omdoc
 REQUIRES = helm-cic_proof_checking
 PREDICATES =
 
-INTERFACE_FILES =  doubleTypeInference.mli cic2acic.mli content.mli \
-                   contentPp.mli
+INTERFACE_FILES =  eta_fixing.mli doubleTypeInference.mli cic2acic.mli \
+                   content.mli contentPp.mli content2cic.mli
 IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
 
 EXTRA_OBJECTS_TO_INSTALL = \
diff --git a/helm/gTopLevel/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml
similarity index 100%
rename from helm/gTopLevel/content2cic.ml
rename to helm/ocaml/cic_omdoc/content2cic.ml
diff --git a/helm/gTopLevel/content2cic.mli b/helm/ocaml/cic_omdoc/content2cic.mli
similarity index 100%
rename from helm/gTopLevel/content2cic.mli
rename to helm/ocaml/cic_omdoc/content2cic.mli
diff --git a/helm/gTopLevel/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml
similarity index 100%
rename from helm/gTopLevel/eta_fixing.ml
rename to helm/ocaml/cic_omdoc/eta_fixing.ml
diff --git a/helm/gTopLevel/eta_fixing.mli b/helm/ocaml/cic_omdoc/eta_fixing.mli
similarity index 100%
rename from helm/gTopLevel/eta_fixing.mli
rename to helm/ocaml/cic_omdoc/eta_fixing.mli
-- 
2.39.2