From 4bcd14a9ed245ccae631697a05ff5a377c02b179 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 20 Jul 2003 11:23:58 +0000 Subject: [PATCH] cic_transformations factorized into cic_omdoc and cic_transformations. --- helm/ocaml/.cvsignore | 1 + helm/ocaml/META.helm-cic_omdoc.src | 4 ++ helm/ocaml/META.helm-cic_transformations.src | 2 +- helm/ocaml/Makefile.in | 2 +- helm/ocaml/cic_omdoc/.depend | 9 +++++ helm/ocaml/cic_omdoc/Makefile | 12 ++++++ .../cic2acic.ml | 0 .../cic2acic.mli | 0 .../content.ml | 0 .../content.mli | 0 .../contentPp.ml | 0 .../contentPp.mli | 0 .../doubleTypeInference.ml | 0 .../doubleTypeInference.mli | 0 helm/ocaml/cic_proof_checking/Makefile | 6 +-- helm/ocaml/cic_transformations/.depend | 38 +++++++------------ helm/ocaml/cic_transformations/Makefile | 11 +++--- 17 files changed, 49 insertions(+), 36 deletions(-) create mode 100644 helm/ocaml/META.helm-cic_omdoc.src create mode 100644 helm/ocaml/cic_omdoc/.depend create mode 100644 helm/ocaml/cic_omdoc/Makefile rename helm/ocaml/{cic_transformations => cic_omdoc}/cic2acic.ml (100%) rename helm/ocaml/{cic_transformations => cic_omdoc}/cic2acic.mli (100%) rename helm/ocaml/{cic_transformations => cic_omdoc}/content.ml (100%) rename helm/ocaml/{cic_transformations => cic_omdoc}/content.mli (100%) rename helm/ocaml/{cic_transformations => cic_omdoc}/contentPp.ml (100%) rename helm/ocaml/{cic_transformations => cic_omdoc}/contentPp.mli (100%) rename helm/ocaml/{cic_transformations => cic_omdoc}/doubleTypeInference.ml (100%) rename helm/ocaml/{cic_transformations => cic_omdoc}/doubleTypeInference.mli (100%) diff --git a/helm/ocaml/.cvsignore b/helm/ocaml/.cvsignore index 53ffeac63..3a94cf124 100644 --- a/helm/ocaml/.cvsignore +++ b/helm/ocaml/.cvsignore @@ -16,6 +16,7 @@ META.helm-tactics META.helm-urimanager META.helm-xml META.helm-cic_transformations +META.helm-cic_omdoc Makefile Makefile.common autom4te.cache diff --git a/helm/ocaml/META.helm-cic_omdoc.src b/helm/ocaml/META.helm-cic_omdoc.src new file mode 100644 index 000000000..313d19cd2 --- /dev/null +++ b/helm/ocaml/META.helm-cic_omdoc.src @@ -0,0 +1,4 @@ +requires="helm-cic_proof_checking" +version="0.0.1" +archive(byte)="cic_omdoc.cma" +archive(native)="cic_omdoc.cmxa" diff --git a/helm/ocaml/META.helm-cic_transformations.src b/helm/ocaml/META.helm-cic_transformations.src index 1888f9d39..44bb0999c 100644 --- a/helm/ocaml/META.helm-cic_transformations.src +++ b/helm/ocaml/META.helm-cic_transformations.src @@ -1,4 +1,4 @@ -requires="helm-xml helm-cic_proof_checking gdome2-xslt" +requires="helm-xml helm-cic_proof_checking helm-cic_omdoc gdome2-xslt" version="0.0.1" archive(byte)="cic_transformations.cma" archive(native)="cic_transformations.cmxa" diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in index aaf8595b1..8eae88814 100644 --- a/helm/ocaml/Makefile.in +++ b/helm/ocaml/Makefile.in @@ -2,7 +2,7 @@ MODULES = xml urimanager getter pxp cic cic_annotations cic_annotations_cache \ cic_cache cic_proof_checking cic_textual_parser \ tex_cic_textual_parser cic_unification mathql mathql_interpreter \ - mathql_generator tactics cic_transformations + mathql_generator cic_omdoc tactics cic_transformations OCAMLFIND_DEST_DIR = @OCAMLFIND_DEST_DIR@ OCAMLFIND_META_DIR = @OCAMLFIND_META_DIR@ diff --git a/helm/ocaml/cic_omdoc/.depend b/helm/ocaml/cic_omdoc/.depend new file mode 100644 index 000000000..1ec905424 --- /dev/null +++ b/helm/ocaml/cic_omdoc/.depend @@ -0,0 +1,9 @@ +contentPp.cmi: content.cmi +doubleTypeInference.cmo: doubleTypeInference.cmi +doubleTypeInference.cmx: doubleTypeInference.cmi +cic2acic.cmo: doubleTypeInference.cmi cic2acic.cmi +cic2acic.cmx: doubleTypeInference.cmx cic2acic.cmi +content.cmo: content.cmi +content.cmx: content.cmi +contentPp.cmo: content.cmi contentPp.cmi +contentPp.cmx: content.cmx contentPp.cmi diff --git a/helm/ocaml/cic_omdoc/Makefile b/helm/ocaml/cic_omdoc/Makefile new file mode 100644 index 000000000..0fbb566ae --- /dev/null +++ b/helm/ocaml/cic_omdoc/Makefile @@ -0,0 +1,12 @@ +PACKAGE = cic_omdoc +REQUIRES = helm-cic_proof_checking +PREDICATES = + +INTERFACE_FILES = doubleTypeInference.mli cic2acic.mli content.mli \ + contentPp.mli +IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) + +EXTRA_OBJECTS_TO_INSTALL = \ +EXTRA_OBJECTS_TO_CLEAN = + +include ../Makefile.common diff --git a/helm/ocaml/cic_transformations/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml similarity index 100% rename from helm/ocaml/cic_transformations/cic2acic.ml rename to helm/ocaml/cic_omdoc/cic2acic.ml diff --git a/helm/ocaml/cic_transformations/cic2acic.mli b/helm/ocaml/cic_omdoc/cic2acic.mli similarity index 100% rename from helm/ocaml/cic_transformations/cic2acic.mli rename to helm/ocaml/cic_omdoc/cic2acic.mli diff --git a/helm/ocaml/cic_transformations/content.ml b/helm/ocaml/cic_omdoc/content.ml similarity index 100% rename from helm/ocaml/cic_transformations/content.ml rename to helm/ocaml/cic_omdoc/content.ml diff --git a/helm/ocaml/cic_transformations/content.mli b/helm/ocaml/cic_omdoc/content.mli similarity index 100% rename from helm/ocaml/cic_transformations/content.mli rename to helm/ocaml/cic_omdoc/content.mli diff --git a/helm/ocaml/cic_transformations/contentPp.ml b/helm/ocaml/cic_omdoc/contentPp.ml similarity index 100% rename from helm/ocaml/cic_transformations/contentPp.ml rename to helm/ocaml/cic_omdoc/contentPp.ml diff --git a/helm/ocaml/cic_transformations/contentPp.mli b/helm/ocaml/cic_omdoc/contentPp.mli similarity index 100% rename from helm/ocaml/cic_transformations/contentPp.mli rename to helm/ocaml/cic_omdoc/contentPp.mli diff --git a/helm/ocaml/cic_transformations/doubleTypeInference.ml b/helm/ocaml/cic_omdoc/doubleTypeInference.ml similarity index 100% rename from helm/ocaml/cic_transformations/doubleTypeInference.ml rename to helm/ocaml/cic_omdoc/doubleTypeInference.ml diff --git a/helm/ocaml/cic_transformations/doubleTypeInference.mli b/helm/ocaml/cic_omdoc/doubleTypeInference.mli similarity index 100% rename from helm/ocaml/cic_transformations/doubleTypeInference.mli rename to helm/ocaml/cic_omdoc/doubleTypeInference.mli diff --git a/helm/ocaml/cic_proof_checking/Makefile b/helm/ocaml/cic_proof_checking/Makefile index 0259effd1..0de0fcda0 100644 --- a/helm/ocaml/cic_proof_checking/Makefile +++ b/helm/ocaml/cic_proof_checking/Makefile @@ -4,9 +4,9 @@ PREDICATES = REDUCTION_IMPLEMENTATION = cicReductionMachine.ml -INTERFACE_FILES = logger.mli cicEnvironment.mli cicPp.mli cicSubstitution.mli \ - cicMiniReduction.mli cicReductionNaif.mli cicReduction.mli \ - cicTypeChecker.mli +INTERFACE_FILES = logger.mli cicEnvironment.mli cicPp.mli cicSubstitution.mli \ + cicMiniReduction.mli cicReductionNaif.mli cicReduction.mli \ + cicTypeChecker.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) # Metadata tools only need zeta-reduction diff --git a/helm/ocaml/cic_transformations/.depend b/helm/ocaml/cic_transformations/.depend index 8dee5ae2b..459aa8c8b 100644 --- a/helm/ocaml/cic_transformations/.depend +++ b/helm/ocaml/cic_transformations/.depend @@ -1,32 +1,20 @@ -cic2Xml.cmi: cic2acic.cmi -cic2content.cmi: cic2acic.cmi content.cmi -contentPp.cmi: content.cmi cexpr2pres.cmi: content_expressions.cmi mpresentation.cmi -content2pres.cmi: content.cmi mpresentation.cmi +content2pres.cmi: mpresentation.cmi cexpr2pres_hashtbl.cmi: content_expressions.cmi mpresentation.cmi -applyStylesheets.cmi: cic2acic.cmi -doubleTypeInference.cmo: doubleTypeInference.cmi -doubleTypeInference.cmx: doubleTypeInference.cmi -cic2acic.cmo: doubleTypeInference.cmi cic2acic.cmi -cic2acic.cmx: doubleTypeInference.cmx cic2acic.cmi -content.cmo: content.cmi -content.cmx: content.cmi -cic2Xml.cmo: cic2acic.cmi cic2Xml.cmi -cic2Xml.cmx: cic2acic.cmx cic2Xml.cmi -cic2content.cmo: cic2acic.cmi content.cmi cic2content.cmi -cic2content.cmx: cic2acic.cmx content.cmx cic2content.cmi -content_expressions.cmo: cic2acic.cmi content_expressions.cmi -content_expressions.cmx: cic2acic.cmx content_expressions.cmi -contentPp.cmo: content.cmi contentPp.cmi -contentPp.cmx: content.cmx contentPp.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 mpresentation.cmx: mpresentation.cmi cexpr2pres.cmo: content_expressions.cmi mpresentation.cmi cexpr2pres.cmi cexpr2pres.cmx: content_expressions.cmx mpresentation.cmx cexpr2pres.cmi -content2pres.cmo: cexpr2pres.cmi content.cmi content_expressions.cmi \ - mpresentation.cmi content2pres.cmi -content2pres.cmx: cexpr2pres.cmx content.cmx content_expressions.cmx \ - mpresentation.cmx content2pres.cmi +content2pres.cmo: cexpr2pres.cmi content_expressions.cmi mpresentation.cmi \ + content2pres.cmi +content2pres.cmx: cexpr2pres.cmx content_expressions.cmx mpresentation.cmx \ + content2pres.cmi cexpr2pres_hashtbl.cmo: cexpr2pres.cmi content_expressions.cmi \ mpresentation.cmi cexpr2pres_hashtbl.cmi cexpr2pres_hashtbl.cmx: cexpr2pres.cmx content_expressions.cmx \ @@ -35,8 +23,8 @@ misc.cmo: misc.cmi misc.cmx: misc.cmi xml2Gdome.cmo: xml2Gdome.cmi xml2Gdome.cmx: xml2Gdome.cmi -sequentPp.cmo: cic2Xml.cmi cic2acic.cmi sequentPp.cmi -sequentPp.cmx: cic2Xml.cmx cic2acic.cmx sequentPp.cmi +sequentPp.cmo: cic2Xml.cmi sequentPp.cmi +sequentPp.cmx: cic2Xml.cmx sequentPp.cmi applyStylesheets.cmo: cic2Xml.cmi misc.cmi sequentPp.cmi xml2Gdome.cmi \ applyStylesheets.cmi applyStylesheets.cmx: cic2Xml.cmx misc.cmx sequentPp.cmx xml2Gdome.cmx \ diff --git a/helm/ocaml/cic_transformations/Makefile b/helm/ocaml/cic_transformations/Makefile index 126e250ba..e1581421e 100644 --- a/helm/ocaml/cic_transformations/Makefile +++ b/helm/ocaml/cic_transformations/Makefile @@ -1,12 +1,11 @@ PACKAGE = cic_transformations -REQUIRES = helm-xml helm-cic_proof_checking gdome2-xslt +REQUIRES = helm-xml helm-cic_proof_checking helm-cic_omdoc gdome2-xslt PREDICATES = -INTERFACE_FILES = doubleTypeInference.mli cic2acic.mli content.mli \ - cic2Xml.mli cic2content.mli content_expressions.mli \ - contentPp.mli mpresentation.mli cexpr2pres.mli \ - content2pres.mli cexpr2pres_hashtbl.mli misc.mli \ - xml2Gdome.mli sequentPp.mli applyStylesheets.mli +INTERFACE_FILES = cic2Xml.mli cic2content.mli content_expressions.mli \ + mpresentation.mli cexpr2pres.mli content2pres.mli \ + cexpr2pres_hashtbl.mli misc.mli xml2Gdome.mli sequentPp.mli \ + applyStylesheets.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = -- 2.39.2