From 9e781c8957ff049e7bba65e1d611e5f007b02fb5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 20 Jul 2003 15:37:04 +0000 Subject: [PATCH] cic2content.ml* moved from cic_transformations to cic_omdoc. --- helm/ocaml/cic_omdoc/.depend | 3 +++ helm/ocaml/cic_omdoc/Makefile | 2 +- helm/ocaml/{cic_transformations => cic_omdoc}/cic2content.ml | 2 -- helm/ocaml/{cic_transformations => cic_omdoc}/cic2content.mli | 0 helm/ocaml/cic_transformations/.depend | 2 -- helm/ocaml/cic_transformations/Makefile | 2 +- 6 files changed, 5 insertions(+), 6 deletions(-) rename helm/ocaml/{cic_transformations => cic_omdoc}/cic2content.ml (99%) rename helm/ocaml/{cic_transformations => cic_omdoc}/cic2content.mli (100%) diff --git a/helm/ocaml/cic_omdoc/.depend b/helm/ocaml/cic_omdoc/.depend index d12896d47..5dfc55b8a 100644 --- a/helm/ocaml/cic_omdoc/.depend +++ b/helm/ocaml/cic_omdoc/.depend @@ -1,4 +1,5 @@ contentPp.cmi: content.cmi +cic2content.cmi: cic2acic.cmi content.cmi content2cic.cmi: content.cmi eta_fixing.cmo: eta_fixing.cmi eta_fixing.cmx: eta_fixing.cmi @@ -10,5 +11,7 @@ content.cmo: content.cmi content.cmx: content.cmi contentPp.cmo: content.cmi contentPp.cmi contentPp.cmx: content.cmx contentPp.cmi +cic2content.cmo: cic2acic.cmi content.cmi cic2content.cmi +cic2content.cmx: cic2acic.cmx content.cmx cic2content.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 e1e081ac6..33f1b3f07 100644 --- a/helm/ocaml/cic_omdoc/Makefile +++ b/helm/ocaml/cic_omdoc/Makefile @@ -3,7 +3,7 @@ REQUIRES = helm-cic_proof_checking PREDICATES = INTERFACE_FILES = eta_fixing.mli doubleTypeInference.mli cic2acic.mli \ - content.mli contentPp.mli content2cic.mli + content.mli contentPp.mli cic2content.mli content2cic.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = \ diff --git a/helm/ocaml/cic_transformations/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml similarity index 99% rename from helm/ocaml/cic_transformations/cic2content.ml rename to helm/ocaml/cic_omdoc/cic2content.ml index 3fd8422cc..82f0005f5 100644 --- a/helm/ocaml/cic_transformations/cic2content.ml +++ b/helm/ocaml/cic_omdoc/cic2content.ml @@ -354,9 +354,7 @@ Not_a_proof exception *) and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t = let rec aux ?(name = None) t = let module C = Cic in - let module X = Xml in let module K = Content in - let module U = UriManager in let module C2A = Cic2acic in let t1 = match t with diff --git a/helm/ocaml/cic_transformations/cic2content.mli b/helm/ocaml/cic_omdoc/cic2content.mli similarity index 100% rename from helm/ocaml/cic_transformations/cic2content.mli rename to helm/ocaml/cic_omdoc/cic2content.mli diff --git a/helm/ocaml/cic_transformations/.depend b/helm/ocaml/cic_transformations/.depend index 459aa8c8b..c7ccf7049 100644 --- a/helm/ocaml/cic_transformations/.depend +++ b/helm/ocaml/cic_transformations/.depend @@ -3,8 +3,6 @@ content2pres.cmi: mpresentation.cmi cexpr2pres_hashtbl.cmi: content_expressions.cmi mpresentation.cmi cic2Xml.cmo: cic2Xml.cmi cic2Xml.cmx: cic2Xml.cmi -cic2content.cmo: cic2content.cmi -cic2content.cmx: cic2content.cmi content_expressions.cmo: content_expressions.cmi content_expressions.cmx: content_expressions.cmi mpresentation.cmo: mpresentation.cmi diff --git a/helm/ocaml/cic_transformations/Makefile b/helm/ocaml/cic_transformations/Makefile index e1581421e..3a3630640 100644 --- a/helm/ocaml/cic_transformations/Makefile +++ b/helm/ocaml/cic_transformations/Makefile @@ -2,7 +2,7 @@ PACKAGE = cic_transformations REQUIRES = helm-xml helm-cic_proof_checking helm-cic_omdoc gdome2-xslt PREDICATES = -INTERFACE_FILES = cic2Xml.mli cic2content.mli content_expressions.mli \ +INTERFACE_FILES = cic2Xml.mli content_expressions.mli \ mpresentation.mli cexpr2pres.mli content2pres.mli \ cexpr2pres_hashtbl.mli misc.mli xml2Gdome.mli sequentPp.mli \ applyStylesheets.mli -- 2.39.2