From aa0d60227b785da3355b31519ba11cb4fbd2c925 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 8 Jan 2006 18:00:22 +0000 Subject: [PATCH] Added $Id$ to every .ml file. --- helm/matita/applyTransformation.ml | 2 ++ helm/matita/dump_moo.ml | 2 ++ helm/matita/matita.ml | 2 ++ helm/matita/matitaEngine.ml | 2 ++ helm/matita/matitaExcPp.ml | 2 ++ helm/matita/matitaGtkMisc.ml | 2 ++ helm/matita/matitaGui.ml | 2 ++ helm/matita/matitaInit.ml | 2 ++ helm/matita/matitaMathView.ml | 2 ++ helm/matita/matitaMisc.ml | 2 ++ helm/matita/matitaScript.ml | 2 ++ helm/matita/matitaTypes.ml | 2 ++ helm/matita/matitac.ml | 2 ++ helm/matita/matitacLib.ml | 2 ++ helm/matita/matitaclean.ml | 2 ++ helm/matita/matitadep.ml | 2 ++ helm/matita/matitamake.ml | 2 ++ helm/matita/matitamakeLib.ml | 2 ++ helm/matita/matitatop.ml | 2 ++ helm/ocaml/acic_content/acic2astMatcher.ml | 2 ++ helm/ocaml/acic_content/acic2content.ml | 2 ++ helm/ocaml/acic_content/cicNotationEnv.ml | 2 ++ helm/ocaml/acic_content/cicNotationPp.ml | 2 ++ helm/ocaml/acic_content/cicNotationPt.ml | 2 ++ helm/ocaml/acic_content/cicNotationUtil.ml | 2 ++ helm/ocaml/acic_content/content.ml | 2 ++ helm/ocaml/acic_content/content2cic.ml | 2 ++ helm/ocaml/acic_content/contentPp.ml | 2 ++ helm/ocaml/acic_content/termAcicContent.ml | 2 ++ helm/ocaml/cic/cic.ml | 2 ++ helm/ocaml/cic/cicParser.ml | 2 ++ helm/ocaml/cic/cicUniv.ml | 2 ++ helm/ocaml/cic/cicUtil.ml | 2 ++ helm/ocaml/cic/deannotate.ml | 2 ++ helm/ocaml/cic/discrimination_tree.ml | 2 ++ helm/ocaml/cic/helmLibraryObjects.ml | 27 +++++++++++++++++++ helm/ocaml/cic/libraryObjects.ml | 2 ++ helm/ocaml/cic/path_indexing.ml | 2 ++ helm/ocaml/cic/test.ml | 2 ++ helm/ocaml/cic/unshare.ml | 2 ++ helm/ocaml/cic_acic/cic2Xml.ml | 2 ++ helm/ocaml/cic_acic/cic2acic.ml | 2 ++ helm/ocaml/cic_acic/doubleTypeInference.ml | 2 ++ helm/ocaml/cic_acic/eta_fixing.ml | 2 ++ helm/ocaml/cic_disambiguation/disambiguate.ml | 2 ++ .../cic_disambiguation/disambiguateChoices.ml | 2 ++ .../cic_disambiguation/disambiguateTypes.ml | 2 ++ .../cic_disambiguation/number_notation.ml | 2 ++ .../cic_proof_checking/cicEnvironment.ml | 1 + helm/ocaml/cic_proof_checking/cicLogger.ml | 2 ++ .../cic_proof_checking/cicMiniReduction.ml | 2 ++ helm/ocaml/cic_proof_checking/cicPp.ml | 2 ++ helm/ocaml/cic_proof_checking/cicReduction.ml | 2 ++ .../cic_proof_checking/cicSubstitution.ml | 2 ++ .../cic_proof_checking/cicTypeChecker.ml | 2 ++ helm/ocaml/cic_proof_checking/cicUnivUtils.ml | 2 ++ .../cic_proof_checking/freshNamesGenerator.ml | 2 ++ helm/ocaml/cic_unification/cicMetaSubst.ml | 2 ++ helm/ocaml/cic_unification/cicMkImplicit.ml | 2 ++ helm/ocaml/cic_unification/cicRefine.ml | 2 ++ helm/ocaml/cic_unification/cicUnification.ml | 2 ++ helm/ocaml/content_pres/box.ml | 2 ++ helm/ocaml/content_pres/boxPp.ml | 2 ++ helm/ocaml/content_pres/cicNotationLexer.ml | 2 ++ helm/ocaml/content_pres/cicNotationParser.ml | 2 ++ helm/ocaml/content_pres/cicNotationPres.ml | 2 ++ helm/ocaml/content_pres/content2pres.ml | 2 ++ .../ocaml/content_pres/content2presMatcher.ml | 2 ++ helm/ocaml/content_pres/mpresentation.ml | 2 ++ helm/ocaml/content_pres/renderingAttrs.ml | 2 ++ helm/ocaml/content_pres/sequent2pres.ml | 2 ++ helm/ocaml/content_pres/termContentPres.ml | 2 ++ helm/ocaml/content_pres/test_lexer.ml | 2 ++ helm/ocaml/extlib/hExtlib.ml | 1 + helm/ocaml/extlib/hLog.ml | 2 ++ helm/ocaml/extlib/hMarshal.ml | 2 ++ helm/ocaml/extlib/patternMatcher.ml | 2 ++ helm/ocaml/getter/http_getter.ml | 2 ++ helm/ocaml/getter/http_getter_common.ml | 2 ++ helm/ocaml/getter/http_getter_const.ml | 2 ++ helm/ocaml/getter/http_getter_env.ml | 2 ++ helm/ocaml/getter/http_getter_logger.ml | 2 ++ helm/ocaml/getter/http_getter_misc.ml | 2 ++ helm/ocaml/getter/http_getter_storage.ml | 2 ++ helm/ocaml/getter/http_getter_types.ml | 2 ++ helm/ocaml/getter/http_getter_wget.ml | 2 ++ helm/ocaml/getter/test.ml | 1 + helm/ocaml/grafite/grafiteAst.ml | 2 ++ helm/ocaml/grafite/grafiteAstPp.ml | 2 ++ helm/ocaml/grafite/grafiteMarshal.ml | 2 ++ helm/ocaml/grafite_engine/grafiteEngine.ml | 2 ++ helm/ocaml/grafite_engine/grafiteMisc.ml | 2 ++ helm/ocaml/grafite_engine/grafiteSync.ml | 2 ++ helm/ocaml/grafite_engine/grafiteTypes.ml | 2 ++ helm/ocaml/grafite_parser/cicNotation2.ml | 2 ++ .../grafite_parser/dependenciesParser.ml | 2 ++ .../grafite_parser/grafiteDisambiguate.ml | 2 ++ .../grafite_parser/grafiteDisambiguator.ml | 2 ++ helm/ocaml/grafite_parser/grafiteParser.ml | 2 ++ helm/ocaml/grafite_parser/print_grammar.ml | 2 ++ helm/ocaml/grafite_parser/test_dep.ml | 2 ++ helm/ocaml/grafite_parser/test_parser.ml | 2 ++ helm/ocaml/hbugs/broker.ml | 2 ++ helm/ocaml/hbugs/client.ml | 2 ++ helm/ocaml/hbugs/hbugs_broker_registry.ml | 2 ++ helm/ocaml/hbugs/hbugs_client.ml | 2 ++ helm/ocaml/hbugs/hbugs_common.ml | 2 ++ helm/ocaml/hbugs/hbugs_id_generator.ml | 2 ++ helm/ocaml/hbugs/hbugs_messages.ml | 2 ++ helm/ocaml/hbugs/hbugs_misc.ml | 2 ++ helm/ocaml/hbugs/hbugs_tutors.ml | 2 ++ .../ocaml/hbugs/search_pattern_apply_tutor.ml | 1 + helm/ocaml/hgdome/domMisc.ml | 2 ++ helm/ocaml/hgdome/xml2Gdome.ml | 2 ++ helm/ocaml/hmysql/hMysql.ml | 2 ++ helm/ocaml/lexicon/cicNotation.ml | 2 ++ helm/ocaml/lexicon/disambiguatePp.ml | 2 ++ helm/ocaml/lexicon/lexiconAst.ml | 2 ++ helm/ocaml/lexicon/lexiconAstPp.ml | 2 ++ helm/ocaml/lexicon/lexiconEngine.ml | 2 ++ helm/ocaml/lexicon/lexiconMarshal.ml | 2 ++ helm/ocaml/lexicon/lexiconSync.ml | 2 ++ helm/ocaml/library/cicCoercion.ml | 2 ++ helm/ocaml/library/cicElim.ml | 2 ++ helm/ocaml/library/cicRecord.ml | 2 ++ helm/ocaml/library/coercDb.ml | 2 ++ helm/ocaml/library/coercGraph.ml | 2 ++ helm/ocaml/library/libraryClean.ml | 2 ++ helm/ocaml/library/libraryDb.ml | 2 ++ helm/ocaml/library/libraryMisc.ml | 2 ++ helm/ocaml/library/libraryNoDb.ml | 2 ++ helm/ocaml/library/librarySync.ml | 2 ++ helm/ocaml/logger/helmLogger.ml | 1 + helm/ocaml/mathql/mathQL.ml | 2 ++ .../mathql_generator/cGLocateInductive.ml | 2 ++ .../mathql_generator/cGMatchConclusion.ml | 2 ++ .../ocaml/mathql_generator/cGSearchPattern.ml | 2 ++ helm/ocaml/mathql_generator/mQGTypes.ml | 2 ++ helm/ocaml/mathql_generator/mQGUtil.ml | 2 ++ .../ocaml/mathql_generator/mQueryGenerator.ml | 2 ++ helm/ocaml/mathql_interpreter/mQIConn.ml | 2 ++ helm/ocaml/mathql_interpreter/mQIMap.ml | 2 ++ helm/ocaml/mathql_interpreter/mQIMySql.ml | 2 ++ helm/ocaml/mathql_interpreter/mQIPostgres.ml | 2 ++ helm/ocaml/mathql_interpreter/mQIProperty.ml | 2 ++ helm/ocaml/mathql_interpreter/mQITypes.ml | 2 ++ helm/ocaml/mathql_interpreter/mQIUtil.ml | 2 ++ .../mathql_interpreter/mQueryInterpreter.ml | 2 ++ helm/ocaml/mathql_interpreter/mQueryUtil.ml | 2 ++ helm/ocaml/metadata/metadataConstraints.ml | 2 ++ helm/ocaml/metadata/metadataDb.ml | 2 ++ helm/ocaml/metadata/metadataExtractor.ml | 2 ++ helm/ocaml/metadata/metadataPp.ml | 2 ++ helm/ocaml/metadata/metadataTypes.ml | 2 ++ helm/ocaml/metadata/sqlStatements.ml | 2 ++ .../ocaml/paramodulation/equality_indexing.ml | 2 ++ helm/ocaml/paramodulation/indexing.ml | 2 ++ helm/ocaml/paramodulation/inference.ml | 2 ++ helm/ocaml/paramodulation/saturate_main.ml | 2 ++ helm/ocaml/paramodulation/saturation.ml | 2 ++ helm/ocaml/paramodulation/test_indexing.ml | 2 ++ helm/ocaml/paramodulation/utils.ml | 2 ++ helm/ocaml/registry/helm_registry.ml | 2 ++ helm/ocaml/registry/test.ml | 2 ++ helm/ocaml/tactics/autoTactic.ml | 2 ++ helm/ocaml/tactics/continuationals.ml | 2 ++ helm/ocaml/tactics/discriminationTactics.ml | 2 ++ helm/ocaml/tactics/eliminationTactics.ml | 2 ++ helm/ocaml/tactics/equalityTactics.ml | 2 ++ helm/ocaml/tactics/fourierR.ml | 2 ++ helm/ocaml/tactics/fwdSimplTactic.ml | 1 + helm/ocaml/tactics/hashtbl_equiv.ml | 1 + helm/ocaml/tactics/history.ml | 2 ++ helm/ocaml/tactics/introductionTactics.ml | 2 ++ helm/ocaml/tactics/inversion.ml | 2 ++ helm/ocaml/tactics/metadataQuery.ml | 2 ++ helm/ocaml/tactics/negationTactics.ml | 2 ++ helm/ocaml/tactics/primitiveTactics.ml | 2 ++ helm/ocaml/tactics/proofEngineHelpers.ml | 2 ++ helm/ocaml/tactics/proofEngineReduction.ml | 1 + .../tactics/proofEngineStructuralRules.ml | 2 ++ helm/ocaml/tactics/proofEngineTypes.ml | 2 ++ helm/ocaml/tactics/reductionTactics.ml | 2 ++ helm/ocaml/tactics/ring.ml | 2 ++ helm/ocaml/tactics/statefulProofEngine.ml | 2 ++ helm/ocaml/tactics/tacticChaser.ml | 2 ++ helm/ocaml/tactics/tacticals.ml | 2 ++ helm/ocaml/tactics/variousTactics.ml | 2 ++ helm/ocaml/thread/extThread.ml | 2 ++ helm/ocaml/thread/threadSafe.ml | 2 ++ helm/ocaml/urimanager/uriManager.ml | 2 ++ helm/ocaml/utf8_macros/make_table.ml | 2 ++ helm/ocaml/utf8_macros/pa_unicode_macro.ml | 2 ++ helm/ocaml/utf8_macros/test.ml | 2 ++ helm/ocaml/utf8_macros/utf8Macro.ml | 2 ++ helm/ocaml/whelp/fwdQueries.ml | 2 ++ helm/ocaml/whelp/whelp.ml | 2 ++ helm/ocaml/xml/test.ml | 1 + helm/ocaml/xml/xml.ml | 2 ++ helm/ocaml/xml/xmlPushParser.ml | 2 ++ helm/ocaml/xmldiff/xmlDiff.ml | 2 ++ 201 files changed, 418 insertions(+) diff --git a/helm/matita/applyTransformation.ml b/helm/matita/applyTransformation.ml index 861fe922d..83e5f3c18 100644 --- a/helm/matita/applyTransformation.ml +++ b/helm/matita/applyTransformation.ml @@ -33,6 +33,8 @@ (* *) (***************************************************************************) +(* $Id$ *) + let mpres_document pres_box = Xml.add_xml_declaration (CicNotationPres.print_box pres_box) diff --git a/helm/matita/dump_moo.ml b/helm/matita/dump_moo.ml index 25b98f424..05c21d40d 100644 --- a/helm/matita/dump_moo.ml +++ b/helm/matita/dump_moo.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf let arg_spec = diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 29df1c3d1..9e96651fe 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf open MatitaGtkMisc diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index f5527bec9..6fca24b13 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf let debug = false ;; diff --git a/helm/matita/matitaExcPp.ml b/helm/matita/matitaExcPp.ml index 7183b8c03..28f25fd5c 100644 --- a/helm/matita/matitaExcPp.ml +++ b/helm/matita/matitaExcPp.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf let rec to_string = diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml index 619c1eadb..f5b578ce6 100644 --- a/helm/matita/matitaGtkMisc.ml +++ b/helm/matita/matitaGtkMisc.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + exception PopupClosed open Printf diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 570769102..a10493fca 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf open MatitaGeneratedGui diff --git a/helm/matita/matitaInit.ml b/helm/matita/matitaInit.ml index c47bcb164..086932f6f 100644 --- a/helm/matita/matitaInit.ml +++ b/helm/matita/matitaInit.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf type thingsToInitilaize = diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index bf0f7f8bd..794b849c4 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + open Printf open GrafiteTypes diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index 389ee2325..0c4329e55 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf (** Functions "imported" from Http_getter_misc *) diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 183846ef6..469676fa7 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf open GrafiteTypes diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index d956af009..13543dbb6 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf open GrafiteTypes diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml index 49032a857..5599ba646 100644 --- a/helm/matita/matitac.ml +++ b/helm/matita/matitac.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + let main () = match Filename.basename Sys.argv.(0) with | "matitadep" | "matitadep.opt" -> Matitadep.main () diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml index eeac8d6c9..3567c33f0 100644 --- a/helm/matita/matitacLib.ml +++ b/helm/matita/matitacLib.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf open GrafiteTypes diff --git a/helm/matita/matitaclean.ml b/helm/matita/matitaclean.ml index 912d32cd0..2a47bd1e4 100644 --- a/helm/matita/matitaclean.ml +++ b/helm/matita/matitaclean.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf module UM = UriManager diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml index 0052199ec..fdcc89aa9 100644 --- a/helm/matita/matitadep.ml +++ b/helm/matita/matitadep.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + module GA = GrafiteAst module U = UriManager diff --git a/helm/matita/matitamake.ml b/helm/matita/matitamake.ml index 96fdbfb28..9eab0f6d8 100644 --- a/helm/matita/matitamake.ml +++ b/helm/matita/matitamake.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + module MK = MatitamakeLib ;; let main () = diff --git a/helm/matita/matitamakeLib.ml b/helm/matita/matitamakeLib.ml index 8f164b73a..8eba26fb0 100644 --- a/helm/matita/matitamakeLib.ml +++ b/helm/matita/matitamakeLib.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + let logger = fun mark -> match mark with | `Error -> HLog.error diff --git a/helm/matita/matitatop.ml b/helm/matita/matitatop.ml index bdf9860b1..0aba1e9b5 100644 --- a/helm/matita/matitatop.ml +++ b/helm/matita/matitatop.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + let _ = let _ = Topdirs.dir_quit in Toploop.loop Format.std_formatter; diff --git a/helm/ocaml/acic_content/acic2astMatcher.ml b/helm/ocaml/acic_content/acic2astMatcher.ml index 7575dc8ba..d62786cc7 100644 --- a/helm/ocaml/acic_content/acic2astMatcher.ml +++ b/helm/ocaml/acic_content/acic2astMatcher.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + module Ast = CicNotationPt module Util = CicNotationUtil diff --git a/helm/ocaml/acic_content/acic2content.ml b/helm/ocaml/acic_content/acic2content.ml index 72699f7e3..8f3b13cfd 100644 --- a/helm/ocaml/acic_content/acic2content.ml +++ b/helm/ocaml/acic_content/acic2content.ml @@ -32,6 +32,8 @@ (* *) (**************************************************************************) +(* $Id$ *) + let object_prefix = "obj:";; let declaration_prefix = "decl:";; let definition_prefix = "def:";; diff --git a/helm/ocaml/acic_content/cicNotationEnv.ml b/helm/ocaml/acic_content/cicNotationEnv.ml index 62212f92f..32d4f0df5 100644 --- a/helm/ocaml/acic_content/cicNotationEnv.ml +++ b/helm/ocaml/acic_content/cicNotationEnv.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + module Ast = CicNotationPt type value = diff --git a/helm/ocaml/acic_content/cicNotationPp.ml b/helm/ocaml/acic_content/cicNotationPp.ml index 0813c732a..5dc6fd821 100644 --- a/helm/ocaml/acic_content/cicNotationPp.ml +++ b/helm/ocaml/acic_content/cicNotationPp.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf module Ast = CicNotationPt diff --git a/helm/ocaml/acic_content/cicNotationPt.ml b/helm/ocaml/acic_content/cicNotationPt.ml index d2a32c779..a66aa5feb 100644 --- a/helm/ocaml/acic_content/cicNotationPt.ml +++ b/helm/ocaml/acic_content/cicNotationPt.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + (** CIC Notation Parse Tree *) type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ] diff --git a/helm/ocaml/acic_content/cicNotationUtil.ml b/helm/ocaml/acic_content/cicNotationUtil.ml index 285047de8..8e487ed11 100644 --- a/helm/ocaml/acic_content/cicNotationUtil.ml +++ b/helm/ocaml/acic_content/cicNotationUtil.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + module Ast = CicNotationPt let visit_ast ?(special_k = fun _ -> assert false) k = diff --git a/helm/ocaml/acic_content/content.ml b/helm/ocaml/acic_content/content.ml index 9687e53fc..22733dcaa 100644 --- a/helm/ocaml/acic_content/content.ml +++ b/helm/ocaml/acic_content/content.ml @@ -32,6 +32,8 @@ (* *) (**************************************************************************) +(* $Id$ *) + type id = string;; type joint_recursion_kind = [ `Recursive of int list diff --git a/helm/ocaml/acic_content/content2cic.ml b/helm/ocaml/acic_content/content2cic.ml index 339492d19..9acea81fa 100644 --- a/helm/ocaml/acic_content/content2cic.ml +++ b/helm/ocaml/acic_content/content2cic.ml @@ -32,6 +32,8 @@ (* *) (***************************************************************************) +(* $Id$ *) + exception TO_DO;; let proof2cic deannotate p = diff --git a/helm/ocaml/acic_content/contentPp.ml b/helm/ocaml/acic_content/contentPp.ml index 3967c6216..ca89fad7d 100644 --- a/helm/ocaml/acic_content/contentPp.ml +++ b/helm/ocaml/acic_content/contentPp.ml @@ -32,6 +32,8 @@ (* *) (***************************************************************************) +(* $Id$ *) + exception ContentPpInternalError;; exception NotEnoughElements;; exception TO_DO diff --git a/helm/ocaml/acic_content/termAcicContent.ml b/helm/ocaml/acic_content/termAcicContent.ml index 4cab1346c..fddd777f7 100644 --- a/helm/ocaml/acic_content/termAcicContent.ml +++ b/helm/ocaml/acic_content/termAcicContent.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf module Ast = CicNotationPt diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml index 6e200cc31..64825e505 100644 --- a/helm/ocaml/cic/cic.ml +++ b/helm/ocaml/cic/cic.ml @@ -35,6 +35,8 @@ (* *) (*****************************************************************************) +(* $Id$ *) + (* STUFF TO MANAGE IDENTIFIERS *) type id = string (* the abstract type of the (annotated) node identifiers *) type 'term explicit_named_substitution = (UriManager.uri * 'term) list diff --git a/helm/ocaml/cic/cicParser.ml b/helm/ocaml/cic/cicParser.ml index 68f1257d1..317bcb9f0 100644 --- a/helm/ocaml/cic/cicParser.ml +++ b/helm/ocaml/cic/cicParser.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) diff --git a/helm/ocaml/cic/cicUniv.ml b/helm/ocaml/cic/cicUniv.ml index 1ab577ec8..669025ffe 100644 --- a/helm/ocaml/cic/cicUniv.ml +++ b/helm/ocaml/cic/cicUniv.ml @@ -34,6 +34,8 @@ (* *) (*****************************************************************************) +(* $Id$ *) + (*****************************************************************************) (** switch implementation **) (*****************************************************************************) diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml index 1af68ce39..7c6e3eabe 100644 --- a/helm/ocaml/cic/cicUtil.ml +++ b/helm/ocaml/cic/cicUtil.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf exception Meta_not_found of int diff --git a/helm/ocaml/cic/deannotate.ml b/helm/ocaml/cic/deannotate.ml index 21e591d4e..f04f5aa10 100644 --- a/helm/ocaml/cic/deannotate.ml +++ b/helm/ocaml/cic/deannotate.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + (* converts annotated terms into cic terms (forgetting ids and names) *) let rec deannotate_term = let module C = Cic in diff --git a/helm/ocaml/cic/discrimination_tree.ml b/helm/ocaml/cic/discrimination_tree.ml index 6e2529016..0bef85a8c 100644 --- a/helm/ocaml/cic/discrimination_tree.ml +++ b/helm/ocaml/cic/discrimination_tree.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + module DiscriminationTreeIndexing = functor (A:Set.S) -> struct diff --git a/helm/ocaml/cic/helmLibraryObjects.ml b/helm/ocaml/cic/helmLibraryObjects.ml index defc33f6c..3038582ab 100644 --- a/helm/ocaml/cic/helmLibraryObjects.ml +++ b/helm/ocaml/cic/helmLibraryObjects.ml @@ -1,3 +1,30 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* $Id$ *) + (** {2 Auxiliary functions} *) let uri = UriManager.uri_of_string diff --git a/helm/ocaml/cic/libraryObjects.ml b/helm/ocaml/cic/libraryObjects.ml index 353710708..cc04322fa 100644 --- a/helm/ocaml/cic/libraryObjects.ml +++ b/helm/ocaml/cic/libraryObjects.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + (**** TABLES ****) let default_eq_URIs = diff --git a/helm/ocaml/cic/path_indexing.ml b/helm/ocaml/cic/path_indexing.ml index 81c3583e1..c0e4bb2be 100644 --- a/helm/ocaml/cic/path_indexing.ml +++ b/helm/ocaml/cic/path_indexing.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + (* path indexing implementation *) (* position of the subterm, subterm (Appl are not stored...) *) diff --git a/helm/ocaml/cic/test.ml b/helm/ocaml/cic/test.ml index 134ff789d..e15468f99 100644 --- a/helm/ocaml/cic/test.ml +++ b/helm/ocaml/cic/test.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf let _ = diff --git a/helm/ocaml/cic/unshare.ml b/helm/ocaml/cic/unshare.ml index 522c82562..e198bcd49 100644 --- a/helm/ocaml/cic/unshare.ml +++ b/helm/ocaml/cic/unshare.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + let rec unshare = let module C = Cic in function diff --git a/helm/ocaml/cic_acic/cic2Xml.ml b/helm/ocaml/cic_acic/cic2Xml.ml index 4d5cb00de..7e97dea6f 100644 --- a/helm/ocaml/cic_acic/cic2Xml.ml +++ b/helm/ocaml/cic_acic/cic2Xml.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + (*CSC codice cut & paste da cicPp e xmlcommand *) exception NotImplemented;; diff --git a/helm/ocaml/cic_acic/cic2acic.ml b/helm/ocaml/cic_acic/cic2acic.ml index 79d9bd0da..8540e0e64 100644 --- a/helm/ocaml/cic_acic/cic2acic.ml +++ b/helm/ocaml/cic_acic/cic2acic.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ] let string_of_sort = function diff --git a/helm/ocaml/cic_acic/doubleTypeInference.ml b/helm/ocaml/cic_acic/doubleTypeInference.ml index 98d12ceca..2400653be 100644 --- a/helm/ocaml/cic_acic/doubleTypeInference.ml +++ b/helm/ocaml/cic_acic/doubleTypeInference.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + exception Impossible of int;; exception NotWellTyped of string;; exception WrongUriToConstant of string;; diff --git a/helm/ocaml/cic_acic/eta_fixing.ml b/helm/ocaml/cic_acic/eta_fixing.ml index 75e66d934..22d26e1bd 100644 --- a/helm/ocaml/cic_acic/eta_fixing.ml +++ b/helm/ocaml/cic_acic/eta_fixing.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + exception ReferenceToNonVariable;; let prerr_endline _ = ();; diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 689460973..f320db2cc 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf open DisambiguateTypes diff --git a/helm/ocaml/cic_disambiguation/disambiguateChoices.ml b/helm/ocaml/cic_disambiguation/disambiguateChoices.ml index 71e320428..bdbc93179 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateChoices.ml +++ b/helm/ocaml/cic_disambiguation/disambiguateChoices.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf open DisambiguateTypes diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml index fda6779e2..4a2e43a20 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + (* type term = CicNotationPt.term type tactic = (term, term, GrafiteAst.reduction, string) GrafiteAst.tactic diff --git a/helm/ocaml/cic_disambiguation/number_notation.ml b/helm/ocaml/cic_disambiguation/number_notation.ml index 05800ffac..2b3ce2d60 100644 --- a/helm/ocaml/cic_disambiguation/number_notation.ml +++ b/helm/ocaml/cic_disambiguation/number_notation.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + let _ = DisambiguateChoices.add_num_choice ("natural number", diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml index 00c7f9206..22845725a 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml @@ -35,6 +35,7 @@ (* *) (*****************************************************************************) +(* $Id$ *) (* ************************************************************************** * CicEnvironment SETTINGS (trust and clean_tmp) diff --git a/helm/ocaml/cic_proof_checking/cicLogger.ml b/helm/ocaml/cic_proof_checking/cicLogger.ml index 28d7a8c2c..5921c61b0 100644 --- a/helm/ocaml/cic_proof_checking/cicLogger.ml +++ b/helm/ocaml/cic_proof_checking/cicLogger.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + type msg = [ `Start_type_checking of UriManager.uri | `Type_checking_completed of UriManager.uri diff --git a/helm/ocaml/cic_proof_checking/cicMiniReduction.ml b/helm/ocaml/cic_proof_checking/cicMiniReduction.ml index bbf515a99..5c88713c5 100644 --- a/helm/ocaml/cic_proof_checking/cicMiniReduction.ml +++ b/helm/ocaml/cic_proof_checking/cicMiniReduction.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + let rec letin_nf = let module C = Cic in function diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml index 9242d1fed..53f52272a 100644 --- a/helm/ocaml/cic_proof_checking/cicPp.ml +++ b/helm/ocaml/cic_proof_checking/cicPp.ml @@ -36,6 +36,8 @@ (* *) (*****************************************************************************) +(* $Id$ *) + exception CicPpInternalError;; exception NotEnoughElements;; diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml index 7ba2cffbc..ce4a6d6cb 100644 --- a/helm/ocaml/cic_proof_checking/cicReduction.ml +++ b/helm/ocaml/cic_proof_checking/cicReduction.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + (* TODO unify exceptions *) exception CicReductionInternalError;; diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml index e9ce94eb8..372c66fb8 100644 --- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml +++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + exception CannotSubstInMeta;; exception RelToHiddenHypothesis;; exception ReferenceToVariable;; diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 5da471a6e..cd742d4cd 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + (* TODO factorize functions to frequent errors (e.g. "Unknwon mutual inductive * ...") *) diff --git a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml index ace4f844f..cd1aeba32 100644 --- a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml +++ b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml @@ -34,6 +34,8 @@ (* *) (*****************************************************************************) +(* $Id$ *) + module C = Cic module H = UriManager.UriHashtbl let eq = UriManager.eq diff --git a/helm/ocaml/cic_proof_checking/freshNamesGenerator.ml b/helm/ocaml/cic_proof_checking/freshNamesGenerator.ml index 113edd1ff..99c9e4d76 100755 --- a/helm/ocaml/cic_proof_checking/freshNamesGenerator.ml +++ b/helm/ocaml/cic_proof_checking/freshNamesGenerator.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + let debug_print = fun _ -> () let rec higher_name arity = diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index 718951c68..afd74d756 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + open Printf (* PROFILING *) diff --git a/helm/ocaml/cic_unification/cicMkImplicit.ml b/helm/ocaml/cic_unification/cicMkImplicit.ml index bc60a188d..36679223c 100644 --- a/helm/ocaml/cic_unification/cicMkImplicit.ml +++ b/helm/ocaml/cic_unification/cicMkImplicit.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + (* identity_relocation_list_for_metavariable i canonical_context *) (* returns the identity relocation list, which is the list [1 ; ... ; n] *) (* where n = List.length [canonical_context] *) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 95e6c7ba6..f03752d10 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + open Printf exception RefineFailure of string Lazy.t;; diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 9db77c5d5..b1ef27f4e 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + open Printf exception UnificationFailure of string Lazy.t;; diff --git a/helm/ocaml/content_pres/box.ml b/helm/ocaml/content_pres/box.ml index c11558a27..8b992e041 100644 --- a/helm/ocaml/content_pres/box.ml +++ b/helm/ocaml/content_pres/box.ml @@ -32,6 +32,8 @@ (* *) (*************************************************************************) +(* $Id$ *) + type 'expr box = Text of attr * string diff --git a/helm/ocaml/content_pres/boxPp.ml b/helm/ocaml/content_pres/boxPp.ml index 657f8a9d3..7a2fa9912 100644 --- a/helm/ocaml/content_pres/boxPp.ml +++ b/helm/ocaml/content_pres/boxPp.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + module Pres = Mpresentation (** {2 Pretty printing from BoxML to strings} *) diff --git a/helm/ocaml/content_pres/cicNotationLexer.ml b/helm/ocaml/content_pres/cicNotationLexer.ml index 958b246de..8848a3ce5 100644 --- a/helm/ocaml/content_pres/cicNotationLexer.ml +++ b/helm/ocaml/content_pres/cicNotationLexer.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf exception Error of int * int * string diff --git a/helm/ocaml/content_pres/cicNotationParser.ml b/helm/ocaml/content_pres/cicNotationParser.ml index 066eb813f..5750ad816 100644 --- a/helm/ocaml/content_pres/cicNotationParser.ml +++ b/helm/ocaml/content_pres/cicNotationParser.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf module Ast = CicNotationPt diff --git a/helm/ocaml/content_pres/cicNotationPres.ml b/helm/ocaml/content_pres/cicNotationPres.ml index 3e47cceb9..6412c3f0c 100644 --- a/helm/ocaml/content_pres/cicNotationPres.ml +++ b/helm/ocaml/content_pres/cicNotationPres.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + module Ast = CicNotationPt module Mpres = Mpresentation diff --git a/helm/ocaml/content_pres/content2pres.ml b/helm/ocaml/content_pres/content2pres.ml index 4114d2b51..195ce0f77 100644 --- a/helm/ocaml/content_pres/content2pres.ml +++ b/helm/ocaml/content_pres/content2pres.ml @@ -32,6 +32,8 @@ (* *) (***************************************************************************) +(* $Id$ *) + module P = Mpresentation module B = Box module Con = Content diff --git a/helm/ocaml/content_pres/content2presMatcher.ml b/helm/ocaml/content_pres/content2presMatcher.ml index 4d99040d5..7e080ea69 100644 --- a/helm/ocaml/content_pres/content2presMatcher.ml +++ b/helm/ocaml/content_pres/content2presMatcher.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf module Ast = CicNotationPt diff --git a/helm/ocaml/content_pres/mpresentation.ml b/helm/ocaml/content_pres/mpresentation.ml index 1303d1eb7..1aa5db129 100644 --- a/helm/ocaml/content_pres/mpresentation.ml +++ b/helm/ocaml/content_pres/mpresentation.ml @@ -32,6 +32,8 @@ (* *) (**************************************************************************) +(* $Id$ *) + type 'a mpres = Mi of attr * string | Mn of attr * string diff --git a/helm/ocaml/content_pres/renderingAttrs.ml b/helm/ocaml/content_pres/renderingAttrs.ml index 478ceff95..cc692abe9 100644 --- a/helm/ocaml/content_pres/renderingAttrs.ml +++ b/helm/ocaml/content_pres/renderingAttrs.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + type xml_attribute = string option * string * string type markup = [ `MathML | `BoxML ] diff --git a/helm/ocaml/content_pres/sequent2pres.ml b/helm/ocaml/content_pres/sequent2pres.ml index bc0dfd055..88c804b7d 100644 --- a/helm/ocaml/content_pres/sequent2pres.ml +++ b/helm/ocaml/content_pres/sequent2pres.ml @@ -32,6 +32,8 @@ (* *) (***************************************************************************) +(* $Id$ *) + let p_mtr a b = Mpresentation.Mtr(a,b) let p_mtd a b = Mpresentation.Mtd(a,b) let p_mtable a b = Mpresentation.Mtable(a,b) diff --git a/helm/ocaml/content_pres/termContentPres.ml b/helm/ocaml/content_pres/termContentPres.ml index fedcef6af..4c8bbc7d4 100644 --- a/helm/ocaml/content_pres/termContentPres.ml +++ b/helm/ocaml/content_pres/termContentPres.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf module Ast = CicNotationPt diff --git a/helm/ocaml/content_pres/test_lexer.ml b/helm/ocaml/content_pres/test_lexer.ml index 569e86e44..b032d7f61 100644 --- a/helm/ocaml/content_pres/test_lexer.ml +++ b/helm/ocaml/content_pres/test_lexer.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + let _ = let level = ref "2@" in let ic = ref stdin in diff --git a/helm/ocaml/extlib/hExtlib.ml b/helm/ocaml/extlib/hExtlib.ml index 979b0c519..15a459cdc 100644 --- a/helm/ocaml/extlib/hExtlib.ml +++ b/helm/ocaml/extlib/hExtlib.ml @@ -23,6 +23,7 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) (** PROFILING *) diff --git a/helm/ocaml/extlib/hLog.ml b/helm/ocaml/extlib/hLog.ml index 8d9fbe958..4ad2b5ba4 100644 --- a/helm/ocaml/extlib/hLog.ml +++ b/helm/ocaml/extlib/hLog.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf type log_tag = [ `Debug | `Error | `Message | `Warning ] diff --git a/helm/ocaml/extlib/hMarshal.ml b/helm/ocaml/extlib/hMarshal.ml index 9091343e4..c57886819 100644 --- a/helm/ocaml/extlib/hMarshal.ml +++ b/helm/ocaml/extlib/hMarshal.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + exception Corrupt_file of string exception Format_mismatch of string exception Version_mismatch of string diff --git a/helm/ocaml/extlib/patternMatcher.ml b/helm/ocaml/extlib/patternMatcher.ml index 27b916bfe..c1b436a97 100644 --- a/helm/ocaml/extlib/patternMatcher.ml +++ b/helm/ocaml/extlib/patternMatcher.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf type pattern_kind = Variable | Constructor diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml index 191117a20..61930a4aa 100644 --- a/helm/ocaml/getter/http_getter.ml +++ b/helm/ocaml/getter/http_getter.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf open Http_getter_common diff --git a/helm/ocaml/getter/http_getter_common.ml b/helm/ocaml/getter/http_getter_common.ml index d56cf6909..a29a44de2 100644 --- a/helm/ocaml/getter/http_getter_common.ml +++ b/helm/ocaml/getter/http_getter_common.ml @@ -26,6 +26,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Http_getter_types;; open Printf;; diff --git a/helm/ocaml/getter/http_getter_const.ml b/helm/ocaml/getter/http_getter_const.ml index 00fff4f37..8103efcfa 100644 --- a/helm/ocaml/getter/http_getter_const.ml +++ b/helm/ocaml/getter/http_getter_const.ml @@ -26,6 +26,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf;; let version = "0.4.0" diff --git a/helm/ocaml/getter/http_getter_env.ml b/helm/ocaml/getter/http_getter_env.ml index c12709dcc..764416cea 100644 --- a/helm/ocaml/getter/http_getter_env.ml +++ b/helm/ocaml/getter/http_getter_env.ml @@ -26,6 +26,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf open Http_getter_types diff --git a/helm/ocaml/getter/http_getter_logger.ml b/helm/ocaml/getter/http_getter_logger.ml index f77b5eba8..1d774c102 100644 --- a/helm/ocaml/getter/http_getter_logger.ml +++ b/helm/ocaml/getter/http_getter_logger.ml @@ -26,6 +26,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + let log_level = ref 1 let get_log_level () = !log_level let set_log_level l = log_level := l diff --git a/helm/ocaml/getter/http_getter_misc.ml b/helm/ocaml/getter/http_getter_misc.ml index b7b52bbf6..45403effa 100644 --- a/helm/ocaml/getter/http_getter_misc.ml +++ b/helm/ocaml/getter/http_getter_misc.ml @@ -26,6 +26,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf let file_scheme_prefix = "file://" diff --git a/helm/ocaml/getter/http_getter_storage.ml b/helm/ocaml/getter/http_getter_storage.ml index 3418956ea..9d1378caa 100644 --- a/helm/ocaml/getter/http_getter_storage.ml +++ b/helm/ocaml/getter/http_getter_storage.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf open Http_getter_misc diff --git a/helm/ocaml/getter/http_getter_types.ml b/helm/ocaml/getter/http_getter_types.ml index 172550652..f84ea85a9 100644 --- a/helm/ocaml/getter/http_getter_types.ml +++ b/helm/ocaml/getter/http_getter_types.ml @@ -26,6 +26,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + exception Bad_request of string exception Unresolvable_URI of string exception Invalid_URI of string diff --git a/helm/ocaml/getter/http_getter_wget.ml b/helm/ocaml/getter/http_getter_wget.ml index a6118c82c..2052e7bd5 100644 --- a/helm/ocaml/getter/http_getter_wget.ml +++ b/helm/ocaml/getter/http_getter_wget.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + open Http_getter_types let send cmd = diff --git a/helm/ocaml/getter/test.ml b/helm/ocaml/getter/test.ml index a35ed4d5b..6fa236fd0 100644 --- a/helm/ocaml/getter/test.ml +++ b/helm/ocaml/getter/test.ml @@ -1,3 +1,4 @@ +(* $Id$ *) let _ = Helm_registry.load_from "foo.conf.xml" let fname = Http_getter.getxml ~format:`Normal ~patch_dtd:true Sys.argv.(1) in diff --git a/helm/ocaml/grafite/grafiteAst.ml b/helm/ocaml/grafite/grafiteAst.ml index 12063745f..c9567155d 100644 --- a/helm/ocaml/grafite/grafiteAst.ml +++ b/helm/ocaml/grafite/grafiteAst.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + type direction = [ `LeftToRight | `RightToLeft ] type loc = Token.flocation diff --git a/helm/ocaml/grafite/grafiteAstPp.ml b/helm/ocaml/grafite/grafiteAstPp.ml index 6f927ee13..6abfa4dd6 100644 --- a/helm/ocaml/grafite/grafiteAstPp.ml +++ b/helm/ocaml/grafite/grafiteAstPp.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf open GrafiteAst diff --git a/helm/ocaml/grafite/grafiteMarshal.ml b/helm/ocaml/grafite/grafiteMarshal.ml index 685a7e948..e786d5001 100644 --- a/helm/ocaml/grafite/grafiteMarshal.ml +++ b/helm/ocaml/grafite/grafiteMarshal.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + type ast_command = Cic.obj GrafiteAst.command type moo = ast_command list diff --git a/helm/ocaml/grafite_engine/grafiteEngine.ml b/helm/ocaml/grafite_engine/grafiteEngine.ml index a035a68e1..5614ff23a 100644 --- a/helm/ocaml/grafite_engine/grafiteEngine.ml +++ b/helm/ocaml/grafite_engine/grafiteEngine.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + exception Drop exception IncludedFileNotCompiled of string (* file name *) (* the integer is expected to be the goal the user is currently seeing *) diff --git a/helm/ocaml/grafite_engine/grafiteMisc.ml b/helm/ocaml/grafite_engine/grafiteMisc.ml index 227cd382b..5b86293db 100644 --- a/helm/ocaml/grafite_engine/grafiteMisc.ml +++ b/helm/ocaml/grafite_engine/grafiteMisc.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + let is_empty buri = List.for_all (function diff --git a/helm/ocaml/grafite_engine/grafiteSync.ml b/helm/ocaml/grafite_engine/grafiteSync.ml index 853a827c0..37a3132e7 100644 --- a/helm/ocaml/grafite_engine/grafiteSync.ml +++ b/helm/ocaml/grafite_engine/grafiteSync.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf let add_obj ~basedir uri obj status = diff --git a/helm/ocaml/grafite_engine/grafiteTypes.ml b/helm/ocaml/grafite_engine/grafiteTypes.ml index a13cc074e..0c02e1b6c 100644 --- a/helm/ocaml/grafite_engine/grafiteTypes.ml +++ b/helm/ocaml/grafite_engine/grafiteTypes.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + exception Option_error of string * string exception Statement_error of string exception Command_error of string diff --git a/helm/ocaml/grafite_parser/cicNotation2.ml b/helm/ocaml/grafite_parser/cicNotation2.ml index f978f2971..015d426e7 100644 --- a/helm/ocaml/grafite_parser/cicNotation2.ml +++ b/helm/ocaml/grafite_parser/cicNotation2.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + let load_notation ~include_paths fname = let ic = open_in fname in let lexbuf = Ulexing.from_utf8_channel ic in diff --git a/helm/ocaml/grafite_parser/dependenciesParser.ml b/helm/ocaml/grafite_parser/dependenciesParser.ml index 74805cfa7..fc49de600 100644 --- a/helm/ocaml/grafite_parser/dependenciesParser.ml +++ b/helm/ocaml/grafite_parser/dependenciesParser.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + exception UnableToInclude of string (* statements meaningful for matitadep *) diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguate.ml b/helm/ocaml/grafite_parser/grafiteDisambiguate.ml index 4be748460..3d6f893ee 100644 --- a/helm/ocaml/grafite_parser/grafiteDisambiguate.ml +++ b/helm/ocaml/grafite_parser/grafiteDisambiguate.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + exception BaseUriNotSetYet let singleton = function diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguator.ml b/helm/ocaml/grafite_parser/grafiteDisambiguator.ml index 5258a4963..d05351cd2 100644 --- a/helm/ocaml/grafite_parser/grafiteDisambiguator.ml +++ b/helm/ocaml/grafite_parser/grafiteDisambiguator.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf exception Ambiguous_input diff --git a/helm/ocaml/grafite_parser/grafiteParser.ml b/helm/ocaml/grafite_parser/grafiteParser.ml index d32eb3265..90d1898ea 100644 --- a/helm/ocaml/grafite_parser/grafiteParser.ml +++ b/helm/ocaml/grafite_parser/grafiteParser.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf module Ast = CicNotationPt diff --git a/helm/ocaml/grafite_parser/print_grammar.ml b/helm/ocaml/grafite_parser/print_grammar.ml index d7d6f3c96..6a05865de 100644 --- a/helm/ocaml/grafite_parser/print_grammar.ml +++ b/helm/ocaml/grafite_parser/print_grammar.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Gramext let tex_of_unicode s = diff --git a/helm/ocaml/grafite_parser/test_dep.ml b/helm/ocaml/grafite_parser/test_dep.ml index 90fdcd3b5..2d0f7813f 100644 --- a/helm/ocaml/grafite_parser/test_dep.ml +++ b/helm/ocaml/grafite_parser/test_dep.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + let _ = let ic = ref stdin in let usage = "test_coarse_parser [ file ]" in diff --git a/helm/ocaml/grafite_parser/test_parser.ml b/helm/ocaml/grafite_parser/test_parser.ml index 3b5c8f375..2deef1bd5 100644 --- a/helm/ocaml/grafite_parser/test_parser.ml +++ b/helm/ocaml/grafite_parser/test_parser.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf let _ = Helm_registry.load_from "test_parser.conf.xml" diff --git a/helm/ocaml/hbugs/broker.ml b/helm/ocaml/hbugs/broker.ml index 6b62af946..691f9d11a 100644 --- a/helm/ocaml/hbugs/broker.ml +++ b/helm/ocaml/hbugs/broker.ml @@ -26,6 +26,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Hbugs_types;; open Printf;; diff --git a/helm/ocaml/hbugs/client.ml b/helm/ocaml/hbugs/client.ml index 85972ace3..93114b305 100644 --- a/helm/ocaml/hbugs/client.ml +++ b/helm/ocaml/hbugs/client.ml @@ -26,6 +26,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Hbugs_common;; open Printf;; diff --git a/helm/ocaml/hbugs/hbugs_broker_registry.ml b/helm/ocaml/hbugs/hbugs_broker_registry.ml index 879d746ac..4670b5eca 100644 --- a/helm/ocaml/hbugs/hbugs_broker_registry.ml +++ b/helm/ocaml/hbugs/hbugs_broker_registry.ml @@ -26,6 +26,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Hbugs_misc;; open Hbugs_types;; open Printf;; diff --git a/helm/ocaml/hbugs/hbugs_client.ml b/helm/ocaml/hbugs/hbugs_client.ml index 4613dbf0d..c7b5fae75 100644 --- a/helm/ocaml/hbugs/hbugs_client.ml +++ b/helm/ocaml/hbugs/hbugs_client.ml @@ -26,6 +26,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Hbugs_common;; open Hbugs_types;; open Printf;; diff --git a/helm/ocaml/hbugs/hbugs_common.ml b/helm/ocaml/hbugs/hbugs_common.ml index 6e060de7a..fe2ecfcae 100644 --- a/helm/ocaml/hbugs/hbugs_common.ml +++ b/helm/ocaml/hbugs/hbugs_common.ml @@ -26,6 +26,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Hbugs_types;; open Printf;; diff --git a/helm/ocaml/hbugs/hbugs_id_generator.ml b/helm/ocaml/hbugs/hbugs_id_generator.ml index f535f4739..5b1998ac2 100644 --- a/helm/ocaml/hbugs/hbugs_id_generator.ml +++ b/helm/ocaml/hbugs/hbugs_id_generator.ml @@ -26,6 +26,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + let _ = Random.self_init () let id_length = 32 diff --git a/helm/ocaml/hbugs/hbugs_messages.ml b/helm/ocaml/hbugs/hbugs_messages.ml index a6aa34b31..4767b2aee 100644 --- a/helm/ocaml/hbugs/hbugs_messages.ml +++ b/helm/ocaml/hbugs/hbugs_messages.ml @@ -26,6 +26,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Hbugs_types;; open Printf;; open Pxp_document;; diff --git a/helm/ocaml/hbugs/hbugs_misc.ml b/helm/ocaml/hbugs/hbugs_misc.ml index b826318e0..32b8e8b46 100644 --- a/helm/ocaml/hbugs/hbugs_misc.ml +++ b/helm/ocaml/hbugs/hbugs_misc.ml @@ -26,6 +26,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf;; let rec hashtbl_remove_all tbl key = diff --git a/helm/ocaml/hbugs/hbugs_tutors.ml b/helm/ocaml/hbugs/hbugs_tutors.ml index 7bb732624..6a73e2cc2 100644 --- a/helm/ocaml/hbugs/hbugs_tutors.ml +++ b/helm/ocaml/hbugs/hbugs_tutors.ml @@ -26,6 +26,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Hbugs_types;; open Printf;; diff --git a/helm/ocaml/hbugs/search_pattern_apply_tutor.ml b/helm/ocaml/hbugs/search_pattern_apply_tutor.ml index 1f5dad1bc..79c94beed 100644 --- a/helm/ocaml/hbugs/search_pattern_apply_tutor.ml +++ b/helm/ocaml/hbugs/search_pattern_apply_tutor.ml @@ -1,3 +1,4 @@ +(* $Id$ *) open Hbugs_types;; open Printf;; diff --git a/helm/ocaml/hgdome/domMisc.ml b/helm/ocaml/hgdome/domMisc.ml index 84445e19c..97a15b7f8 100644 --- a/helm/ocaml/hgdome/domMisc.ml +++ b/helm/ocaml/hgdome/domMisc.ml @@ -33,6 +33,8 @@ (* *) (******************************************************************************) +(* $Id$ *) + let domImpl = Gdome.domImplementation () let helm_ns = Gdome.domString "http://www.cs.unibo.it/helm" let xlink_ns = Gdome.domString "http://www.w3.org/1999/xlink" diff --git a/helm/ocaml/hgdome/xml2Gdome.ml b/helm/ocaml/hgdome/xml2Gdome.ml index 3d07bf21c..eb6a7641c 100644 --- a/helm/ocaml/hgdome/xml2Gdome.ml +++ b/helm/ocaml/hgdome/xml2Gdome.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + let document_of_xml (domImplementation : Gdome.domImplementation) strm = let module G = Gdome in let module X = Xml in diff --git a/helm/ocaml/hmysql/hMysql.ml b/helm/ocaml/hmysql/hMysql.ml index c7bfb325e..94f3efe03 100644 --- a/helm/ocaml/hmysql/hMysql.ml +++ b/helm/ocaml/hmysql/hMysql.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + type dbd = Mysql.dbd option type result = Mysql.result option type error_code = Mysql.error_code diff --git a/helm/ocaml/lexicon/cicNotation.ml b/helm/ocaml/lexicon/cicNotation.ml index 0d48ea06d..1d18691ff 100644 --- a/helm/ocaml/lexicon/cicNotation.ml +++ b/helm/ocaml/lexicon/cicNotation.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open LexiconAst type notation_id = diff --git a/helm/ocaml/lexicon/disambiguatePp.ml b/helm/ocaml/lexicon/disambiguatePp.ml index a54e67506..5f6512477 100644 --- a/helm/ocaml/lexicon/disambiguatePp.ml +++ b/helm/ocaml/lexicon/disambiguatePp.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open DisambiguateTypes let alias_of_domain_and_codomain_items domain_item (dsc,_) = diff --git a/helm/ocaml/lexicon/lexiconAst.ml b/helm/ocaml/lexicon/lexiconAst.ml index 13135744e..aed4b0b15 100644 --- a/helm/ocaml/lexicon/lexiconAst.ml +++ b/helm/ocaml/lexicon/lexiconAst.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + type direction = [ `LeftToRight | `RightToLeft ] type loc = Token.flocation diff --git a/helm/ocaml/lexicon/lexiconAstPp.ml b/helm/ocaml/lexicon/lexiconAstPp.ml index 57d22d6b4..e49a66f60 100644 --- a/helm/ocaml/lexicon/lexiconAstPp.ml +++ b/helm/ocaml/lexicon/lexiconAstPp.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf open LexiconAst diff --git a/helm/ocaml/lexicon/lexiconEngine.ml b/helm/ocaml/lexicon/lexiconEngine.ml index 752dabb71..d85ed51d8 100644 --- a/helm/ocaml/lexicon/lexiconEngine.ml +++ b/helm/ocaml/lexicon/lexiconEngine.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + exception IncludedFileNotCompiled of string (* file name *) exception MetadataNotFound of string (* file name *) diff --git a/helm/ocaml/lexicon/lexiconMarshal.ml b/helm/ocaml/lexicon/lexiconMarshal.ml index 8b6ad8312..7b9422db5 100644 --- a/helm/ocaml/lexicon/lexiconMarshal.ml +++ b/helm/ocaml/lexicon/lexiconMarshal.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + type lexicon = LexiconAst.command list let format_name = "lexicon" diff --git a/helm/ocaml/lexicon/lexiconSync.ml b/helm/ocaml/lexicon/lexiconSync.ml index b6d2270fe..d7fa27f90 100644 --- a/helm/ocaml/lexicon/lexiconSync.ml +++ b/helm/ocaml/lexicon/lexiconSync.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + let alias_diff ~from status = let module Map = DisambiguateTypes.Environment in Map.fold diff --git a/helm/ocaml/library/cicCoercion.ml b/helm/ocaml/library/cicCoercion.ml index 981baffce..fe636ee35 100644 --- a/helm/ocaml/library/cicCoercion.ml +++ b/helm/ocaml/library/cicCoercion.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) else () diff --git a/helm/ocaml/library/cicElim.ml b/helm/ocaml/library/cicElim.ml index 74fa6d038..fb3c0655c 100644 --- a/helm/ocaml/library/cicElim.ml +++ b/helm/ocaml/library/cicElim.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf exception Elim_failure of string Lazy.t diff --git a/helm/ocaml/library/cicRecord.ml b/helm/ocaml/library/cicRecord.ml index 85c2ea036..775292ccb 100644 --- a/helm/ocaml/library/cicRecord.ml +++ b/helm/ocaml/library/cicRecord.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + let rec_ty uri leftno = let rec_ty = Cic.MutInd (uri,0,[]) in if leftno = 0 then rec_ty else diff --git a/helm/ocaml/library/coercDb.ml b/helm/ocaml/library/coercDb.ml index ac5067585..01065325f 100644 --- a/helm/ocaml/library/coercDb.ml +++ b/helm/ocaml/library/coercDb.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + type coerc_carr = Uri of UriManager.uri | Sort of Cic.sort | Term of Cic.term exception EqCarrNotImplemented of string Lazy.t exception EqCarrOnNonMetaClosed diff --git a/helm/ocaml/library/coercGraph.ml b/helm/ocaml/library/coercGraph.ml index b3176d093..cd958a8f6 100644 --- a/helm/ocaml/library/coercGraph.ml +++ b/helm/ocaml/library/coercGraph.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + open Printf;; type coercion_search_result = diff --git a/helm/ocaml/library/libraryClean.ml b/helm/ocaml/library/libraryClean.ml index 092527155..d09769fc2 100644 --- a/helm/ocaml/library/libraryClean.ml +++ b/helm/ocaml/library/libraryClean.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf let debug = false diff --git a/helm/ocaml/library/libraryDb.ml b/helm/ocaml/library/libraryDb.ml index 389b7f483..f04043366 100644 --- a/helm/ocaml/library/libraryDb.ml +++ b/helm/ocaml/library/libraryDb.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf ;; let instance = diff --git a/helm/ocaml/library/libraryMisc.ml b/helm/ocaml/library/libraryMisc.ml index 7911789e2..3f1931e42 100644 --- a/helm/ocaml/library/libraryMisc.ml +++ b/helm/ocaml/library/libraryMisc.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + let obj_file_of_baseuri ~basedir ~baseuri = let path = basedir ^ "/xml" ^ Pcre.replace ~pat:"^cic:" ~templ:"" baseuri in path ^ ".moo" diff --git a/helm/ocaml/library/libraryNoDb.ml b/helm/ocaml/library/libraryNoDb.ml index bb1c5bb77..9ac42a5ea 100644 --- a/helm/ocaml/library/libraryNoDb.ml +++ b/helm/ocaml/library/libraryNoDb.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf exception Checksum_failure of string diff --git a/helm/ocaml/library/librarySync.ml b/helm/ocaml/library/librarySync.ml index 1ccc9d30f..fe631edd2 100644 --- a/helm/ocaml/library/librarySync.ml +++ b/helm/ocaml/library/librarySync.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + exception AlreadyDefined of UriManager.uri let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29 diff --git a/helm/ocaml/logger/helmLogger.ml b/helm/ocaml/logger/helmLogger.ml index 7a1e63483..c41674754 100644 --- a/helm/ocaml/logger/helmLogger.ml +++ b/helm/ocaml/logger/helmLogger.ml @@ -1,3 +1,4 @@ +(* $Id$ *) open Printf diff --git a/helm/ocaml/mathql/mathQL.ml b/helm/ocaml/mathql/mathQL.ml index 7e82fe547..2504cfb4f 100644 --- a/helm/ocaml/mathql/mathQL.ml +++ b/helm/ocaml/mathql/mathQL.ml @@ -26,6 +26,8 @@ (* AUTOR: Ferruccio Guidi *) +(* $Id$ *) + (* output data structures ***************************************************) type path = string list (* the name of an attribute *) diff --git a/helm/ocaml/mathql_generator/cGLocateInductive.ml b/helm/ocaml/mathql_generator/cGLocateInductive.ml index 04181fb23..261b29388 100644 --- a/helm/ocaml/mathql_generator/cGLocateInductive.ml +++ b/helm/ocaml/mathql_generator/cGLocateInductive.ml @@ -26,6 +26,8 @@ (* AUTOR: Ferruccio Guidi *) +(* $Id$ *) + exception NotAnInductiveDefinition let get_constraints = function diff --git a/helm/ocaml/mathql_generator/cGMatchConclusion.ml b/helm/ocaml/mathql_generator/cGMatchConclusion.ml index 70dfde475..0a67c2d0d 100644 --- a/helm/ocaml/mathql_generator/cGMatchConclusion.ml +++ b/helm/ocaml/mathql_generator/cGMatchConclusion.ml @@ -26,6 +26,8 @@ (* AUTOR: Ferruccio Guidi *) +(* $Id$ *) + module T = MQGTypes let text_of_entries out entries = diff --git a/helm/ocaml/mathql_generator/cGSearchPattern.ml b/helm/ocaml/mathql_generator/cGSearchPattern.ml index 47345e9f3..1d7e85937 100644 --- a/helm/ocaml/mathql_generator/cGSearchPattern.ml +++ b/helm/ocaml/mathql_generator/cGSearchPattern.ml @@ -34,6 +34,8 @@ (* *) (******************************************************************************) +(* $Id$ *) + module T = MQGTypes module U = MQGUtil diff --git a/helm/ocaml/mathql_generator/mQGTypes.ml b/helm/ocaml/mathql_generator/mQGTypes.ml index a210aa68f..9ed2ce253 100644 --- a/helm/ocaml/mathql_generator/mQGTypes.ml +++ b/helm/ocaml/mathql_generator/mQGTypes.ml @@ -27,6 +27,8 @@ * Claudio Sacerdoti Coen *) +(* $Id$ *) + (* low level types *********************************************************) type uri = string diff --git a/helm/ocaml/mathql_generator/mQGUtil.ml b/helm/ocaml/mathql_generator/mQGUtil.ml index e30742649..7603ab9a6 100644 --- a/helm/ocaml/mathql_generator/mQGUtil.ml +++ b/helm/ocaml/mathql_generator/mQGUtil.ml @@ -26,6 +26,8 @@ (* AUTOR: Ferruccio Guidi *) +(* $Id$ *) + module T = MQGTypes (* low level functions *****************************************************) diff --git a/helm/ocaml/mathql_generator/mQueryGenerator.ml b/helm/ocaml/mathql_generator/mQueryGenerator.ml index dd8b00ae3..784bc11dc 100644 --- a/helm/ocaml/mathql_generator/mQueryGenerator.ml +++ b/helm/ocaml/mathql_generator/mQueryGenerator.ml @@ -26,6 +26,8 @@ (* AUTOR: Ferruccio Guidi *) +(* $Id$ *) + module M = MathQL module T = MQGTypes module U = MQGUtil diff --git a/helm/ocaml/mathql_interpreter/mQIConn.ml b/helm/ocaml/mathql_interpreter/mQIConn.ml index aaf16fac4..270d1f9d0 100644 --- a/helm/ocaml/mathql_interpreter/mQIConn.ml +++ b/helm/ocaml/mathql_interpreter/mQIConn.ml @@ -26,6 +26,8 @@ (* AUTOR: Ferruccio Guidi *) +(* $Id$ *) + type connection = MySQL_C of HMysql.dbd | Postgres_C of Postgres.connection | No_C diff --git a/helm/ocaml/mathql_interpreter/mQIMap.ml b/helm/ocaml/mathql_interpreter/mQIMap.ml index b215f366f..a5b6654c8 100644 --- a/helm/ocaml/mathql_interpreter/mQIMap.ml +++ b/helm/ocaml/mathql_interpreter/mQIMap.ml @@ -26,6 +26,8 @@ (* AUTOR: Ferruccio Guidi *) +(* $Id$ *) + module U = MQueryUtil type pg_map = (MathQL.path * (bool * string * string option)) list diff --git a/helm/ocaml/mathql_interpreter/mQIMySql.ml b/helm/ocaml/mathql_interpreter/mQIMySql.ml index 46f350e21..3380e1f1f 100644 --- a/helm/ocaml/mathql_interpreter/mQIMySql.ml +++ b/helm/ocaml/mathql_interpreter/mQIMySql.ml @@ -26,6 +26,8 @@ (* AUTOR: Ferruccio Guidi *) +(* $Id$ *) + let init () = let module HR = Helm_registry in let host = diff --git a/helm/ocaml/mathql_interpreter/mQIPostgres.ml b/helm/ocaml/mathql_interpreter/mQIPostgres.ml index 916f78732..bef07230f 100644 --- a/helm/ocaml/mathql_interpreter/mQIPostgres.ml +++ b/helm/ocaml/mathql_interpreter/mQIPostgres.ml @@ -26,6 +26,8 @@ (* AUTOR: Ferruccio Guidi *) +(* $Id$ *) + let init () = let connection_string = Helm_registry.get "mathql_interpreter.postgresql_connection_string" diff --git a/helm/ocaml/mathql_interpreter/mQIProperty.ml b/helm/ocaml/mathql_interpreter/mQIProperty.ml index 60a003a32..0e3e2be72 100644 --- a/helm/ocaml/mathql_interpreter/mQIProperty.ml +++ b/helm/ocaml/mathql_interpreter/mQIProperty.ml @@ -26,6 +26,8 @@ (* AUTOR: Ferruccio Guidi *) +(* $Id$ *) + module M = MathQL module C = MQIConn module U = MQIUtil diff --git a/helm/ocaml/mathql_interpreter/mQITypes.ml b/helm/ocaml/mathql_interpreter/mQITypes.ml index 44b21ce18..ad4a8cb1b 100644 --- a/helm/ocaml/mathql_interpreter/mQITypes.ml +++ b/helm/ocaml/mathql_interpreter/mQITypes.ml @@ -26,6 +26,8 @@ (* AUTOR: Ferruccio Guidi *) +(* $Id$ *) + type 'a con = MathQL.pattern * 'a * MathQL.value type 'a con_true = 'a con list diff --git a/helm/ocaml/mathql_interpreter/mQIUtil.ml b/helm/ocaml/mathql_interpreter/mQIUtil.ml index 00f5390b5..3f3fe6591 100644 --- a/helm/ocaml/mathql_interpreter/mQIUtil.ml +++ b/helm/ocaml/mathql_interpreter/mQIUtil.ml @@ -26,6 +26,8 @@ (* AUTOR: Ferruccio Guidi *) +(* $Id$ *) + (* boolean constants *******************************************************) let mql_false = [] diff --git a/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml b/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml index 453b1643c..9280a2c2a 100644 --- a/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml +++ b/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml @@ -26,6 +26,8 @@ (* AUTOR: Ferruccio Guidi *) +(* $Id$ *) + (* contexts *****************************************************************) type svar_context = (MathQL.svar * MathQL.resource_set) list diff --git a/helm/ocaml/mathql_interpreter/mQueryUtil.ml b/helm/ocaml/mathql_interpreter/mQueryUtil.ml index e8344b0d6..6323cc950 100644 --- a/helm/ocaml/mathql_interpreter/mQueryUtil.ml +++ b/helm/ocaml/mathql_interpreter/mQueryUtil.ml @@ -26,6 +26,8 @@ (* AUTOR: Ferruccio Guidi *) +(* $Id$ *) + (* text linearization and parsing *******************************************) let rec txt_list out f s = function diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml index 7bc92eb66..07fcc738b 100644 --- a/helm/ocaml/metadata/metadataConstraints.ml +++ b/helm/ocaml/metadata/metadataConstraints.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf open MetadataTypes diff --git a/helm/ocaml/metadata/metadataDb.ml b/helm/ocaml/metadata/metadataDb.ml index c5fbb79a8..457545dee 100644 --- a/helm/ocaml/metadata/metadataDb.ml +++ b/helm/ocaml/metadata/metadataDb.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open MetadataTypes open Printf diff --git a/helm/ocaml/metadata/metadataExtractor.ml b/helm/ocaml/metadata/metadataExtractor.ml index 50407ac7c..4fbae1ba7 100644 --- a/helm/ocaml/metadata/metadataExtractor.ml +++ b/helm/ocaml/metadata/metadataExtractor.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf open MetadataTypes diff --git a/helm/ocaml/metadata/metadataPp.ml b/helm/ocaml/metadata/metadataPp.ml index acf425ce1..373ec540f 100644 --- a/helm/ocaml/metadata/metadataPp.ml +++ b/helm/ocaml/metadata/metadataPp.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf open MetadataTypes diff --git a/helm/ocaml/metadata/metadataTypes.ml b/helm/ocaml/metadata/metadataTypes.ml index 81eb35817..e186b377a 100644 --- a/helm/ocaml/metadata/metadataTypes.ml +++ b/helm/ocaml/metadata/metadataTypes.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + let position_prefix = "http://www.cs.unibo.it/helm/schemas/schema-helm#" (* let position_prefix = "" *) diff --git a/helm/ocaml/metadata/sqlStatements.ml b/helm/ocaml/metadata/sqlStatements.ml index 262188e13..a08073965 100644 --- a/helm/ocaml/metadata/sqlStatements.ml +++ b/helm/ocaml/metadata/sqlStatements.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf;; type tbl = [ `RefObj| `RefSort| `RefRel| `ObjectName| `Hits| `Count] diff --git a/helm/ocaml/paramodulation/equality_indexing.ml b/helm/ocaml/paramodulation/equality_indexing.ml index fd3fa5c32..1dffb6399 100644 --- a/helm/ocaml/paramodulation/equality_indexing.ml +++ b/helm/ocaml/paramodulation/equality_indexing.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + module type EqualityIndex = sig module PosEqSet : Set.S with type elt = Utils.pos * Inference.equality diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml index 523cff882..2d9076ad5 100644 --- a/helm/ocaml/paramodulation/indexing.ml +++ b/helm/ocaml/paramodulation/indexing.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + module Index = Equality_indexing.DT (* discrimination tree based indexing *) (* module Index = Equality_indexing.DT (* path tree based indexing *) diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index 43211ccf9..5a2fd042d 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + open Utils;; diff --git a/helm/ocaml/paramodulation/saturate_main.ml b/helm/ocaml/paramodulation/saturate_main.ml index 758437b76..71aa9beae 100644 --- a/helm/ocaml/paramodulation/saturate_main.ml +++ b/helm/ocaml/paramodulation/saturate_main.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + module Trivial_disambiguate: sig exception Ambiguous_term of string Lazy.t diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index bef39f7b2..e3799983b 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + open Inference;; open Utils;; diff --git a/helm/ocaml/paramodulation/test_indexing.ml b/helm/ocaml/paramodulation/test_indexing.ml index 5681a5d08..ba6b2ebe0 100644 --- a/helm/ocaml/paramodulation/test_indexing.ml +++ b/helm/ocaml/paramodulation/test_indexing.ml @@ -1,3 +1,5 @@ +(* $Id$ *) + open Path_indexing (* diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml index 6ee45f235..70a77c8e8 100644 --- a/helm/ocaml/paramodulation/utils.ml +++ b/helm/ocaml/paramodulation/utils.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + let debug = true;; let debug_print s = if debug then prerr_endline (Lazy.force s);; diff --git a/helm/ocaml/registry/helm_registry.ml b/helm/ocaml/registry/helm_registry.ml index 35726d4c9..42316a27f 100644 --- a/helm/ocaml/registry/helm_registry.ml +++ b/helm/ocaml/registry/helm_registry.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf let debug = false diff --git a/helm/ocaml/registry/test.ml b/helm/ocaml/registry/test.ml index 644b0f0da..d0b91a28c 100644 --- a/helm/ocaml/registry/test.ml +++ b/helm/ocaml/registry/test.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf;; Helm_registry.load_from Sys.argv.(1); Helm_registry.iter ~interpolate:false (fun k v -> printf "%s = %s\n" k v); diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml index 03dd1f254..dc5b8324c 100644 --- a/helm/ocaml/tactics/autoTactic.ml +++ b/helm/ocaml/tactics/autoTactic.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) diff --git a/helm/ocaml/tactics/continuationals.ml b/helm/ocaml/tactics/continuationals.ml index fd965dddd..3ed167a71 100644 --- a/helm/ocaml/tactics/continuationals.ml +++ b/helm/ocaml/tactics/continuationals.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf let debug = false diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml index dd122ee48..9e5bc7f43 100644 --- a/helm/ocaml/tactics/discriminationTactics.ml +++ b/helm/ocaml/tactics/discriminationTactics.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + let debug_print = fun _ -> () let rec injection_tac ~term = diff --git a/helm/ocaml/tactics/eliminationTactics.ml b/helm/ocaml/tactics/eliminationTactics.ml index 17d416ea9..e98bcd3c8 100644 --- a/helm/ocaml/tactics/eliminationTactics.ml +++ b/helm/ocaml/tactics/eliminationTactics.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + module C = Cic module P = PrimitiveTactics module T = Tacticals diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index 5d995c49b..8304d7bb1 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -22,6 +22,8 @@ * For details, see the HELM World-Wide-Web page, * http://cs.unibo.it/helm/. *) + +(* $Id$ *) let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equality = let _rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality status diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml index 32dfb5db2..5418e1149 100644 --- a/helm/ocaml/tactics/fourierR.ml +++ b/helm/ocaml/tactics/fourierR.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + (******************** THE FOURIER TACTIC ***********************) diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml index a40dd42b3..0bae64f6c 100644 --- a/helm/ocaml/tactics/fwdSimplTactic.ml +++ b/helm/ocaml/tactics/fwdSimplTactic.ml @@ -23,6 +23,7 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) module PEH = ProofEngineHelpers module U = CicUniv diff --git a/helm/ocaml/tactics/hashtbl_equiv.ml b/helm/ocaml/tactics/hashtbl_equiv.ml index 543528de6..86448268c 100644 --- a/helm/ocaml/tactics/hashtbl_equiv.ml +++ b/helm/ocaml/tactics/hashtbl_equiv.ml @@ -33,6 +33,7 @@ (* *) (*********************************************************************) +(* $Id$ *) (* the file contains an hash table of objects of the library equivalent to some object in the standard subset; it is diff --git a/helm/ocaml/tactics/history.ml b/helm/ocaml/tactics/history.ml index 3a966b56f..7559f367e 100644 --- a/helm/ocaml/tactics/history.ml +++ b/helm/ocaml/tactics/history.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + exception History_failure class ['a] history size = diff --git a/helm/ocaml/tactics/introductionTactics.ml b/helm/ocaml/tactics/introductionTactics.ml index 6bf8ab6c1..9ed3647c1 100644 --- a/helm/ocaml/tactics/introductionTactics.ml +++ b/helm/ocaml/tactics/introductionTactics.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + let fake_constructor_tac ~n (proof, goal) = let module C = Cic in let module R = CicReduction in diff --git a/helm/ocaml/tactics/inversion.ml b/helm/ocaml/tactics/inversion.ml index 3bedf006a..ca175af94 100644 --- a/helm/ocaml/tactics/inversion.ml +++ b/helm/ocaml/tactics/inversion.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + exception TheTypeOfTheCurrentGoalIsAMetaICannotChooseTheRightElimiantionPrinciple exception NotAnInductiveTypeToEliminate diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index 9385f1c99..b9c053653 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf let nonvar uri = not (UriManager.uri_is_var uri) diff --git a/helm/ocaml/tactics/negationTactics.ml b/helm/ocaml/tactics/negationTactics.ml index 8f05ae436..7ee79e534 100644 --- a/helm/ocaml/tactics/negationTactics.ml +++ b/helm/ocaml/tactics/negationTactics.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + let absurd_tac ~term = let absurd_tac ~term status = let (proof, goal) = status in diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index ca6b0e582..7a732a572 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + open ProofEngineHelpers open ProofEngineTypes diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml index bb6390bdc..cf7df2d58 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.ml +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + exception Bad_pattern of string Lazy.t let new_meta_of_proof ~proof:(_, metasenv, _, _) = diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml index 0a1f13a78..755a09854 100644 --- a/helm/ocaml/tactics/proofEngineReduction.ml +++ b/helm/ocaml/tactics/proofEngineReduction.ml @@ -33,6 +33,7 @@ (* *) (******************************************************************************) +(* $Id$ *) (* The code of this module is derived from the code of CicReduction *) diff --git a/helm/ocaml/tactics/proofEngineStructuralRules.ml b/helm/ocaml/tactics/proofEngineStructuralRules.ml index 8995fbbeb..4677a33ac 100644 --- a/helm/ocaml/tactics/proofEngineStructuralRules.ml +++ b/helm/ocaml/tactics/proofEngineStructuralRules.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + open ProofEngineTypes let clearbody ~hyp = diff --git a/helm/ocaml/tactics/proofEngineTypes.ml b/helm/ocaml/tactics/proofEngineTypes.ml index 7497da7ed..68ea561f9 100644 --- a/helm/ocaml/tactics/proofEngineTypes.ml +++ b/helm/ocaml/tactics/proofEngineTypes.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + (** current proof (proof uri * metas * (in)complete proof * term to be prooved) *) diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml index 4fc192a5b..115faa80b 100644 --- a/helm/ocaml/tactics/reductionTactics.ml +++ b/helm/ocaml/tactics/reductionTactics.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + open ProofEngineTypes (* Note: this code is almost identical to change_tac and diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml index 1d7cc10e6..4c58f1004 100644 --- a/helm/ocaml/tactics/ring.ml +++ b/helm/ocaml/tactics/ring.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + open CicReduction open PrimitiveTactics open ProofEngineTypes diff --git a/helm/ocaml/tactics/statefulProofEngine.ml b/helm/ocaml/tactics/statefulProofEngine.ml index f75442922..9529c897c 100644 --- a/helm/ocaml/tactics/statefulProofEngine.ml +++ b/helm/ocaml/tactics/statefulProofEngine.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + let default_history_size = 20 exception No_goal_left diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml index de356a3d1..cb700f776 100644 --- a/helm/ocaml/tactics/tacticChaser.ml +++ b/helm/ocaml/tactics/tacticChaser.ml @@ -33,6 +33,8 @@ (* *) (*****************************************************************************) +(* $Id$ *) + module MQI = MQueryInterpreter module MQIC = MQIConn module I = MQueryInterpreter diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml index b0a9f452e..a674fe313 100644 --- a/helm/ocaml/tactics/tacticals.ml +++ b/helm/ocaml/tactics/tacticals.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + (* open CicReduction open ProofEngineTypes open UriManager *) diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml index 927552f0a..fc6413eb5 100644 --- a/helm/ocaml/tactics/variousTactics.ml +++ b/helm/ocaml/tactics/variousTactics.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + (* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio chiedere: find dovrebbe restituire una lista di hyp (?) da passare all'utonto con una diff --git a/helm/ocaml/thread/extThread.ml b/helm/ocaml/thread/extThread.ml index 2162251ac..d59cccd26 100644 --- a/helm/ocaml/thread/extThread.ml +++ b/helm/ocaml/thread/extThread.ml @@ -26,6 +26,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + let debug = true let debug_print s = if debug then prerr_endline (Lazy.force s) diff --git a/helm/ocaml/thread/threadSafe.ml b/helm/ocaml/thread/threadSafe.ml index affeae137..afe953370 100644 --- a/helm/ocaml/thread/threadSafe.ml +++ b/helm/ocaml/thread/threadSafe.ml @@ -26,6 +26,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) diff --git a/helm/ocaml/urimanager/uriManager.ml b/helm/ocaml/urimanager/uriManager.ml index b4bf073e2..9ff6a7966 100644 --- a/helm/ocaml/urimanager/uriManager.ml +++ b/helm/ocaml/urimanager/uriManager.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + (* * "cic:/a/b/c.con" => ("cic:/a/b/c.con", id ) * "cic:/a/b/c.ind#xpointer(1/1)" => ("cic:/a/b/c.con#xpointer(1/1)", id) diff --git a/helm/ocaml/utf8_macros/make_table.ml b/helm/ocaml/utf8_macros/make_table.ml index 68309b1c4..4722af1e1 100644 --- a/helm/ocaml/utf8_macros/make_table.ml +++ b/helm/ocaml/utf8_macros/make_table.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf let debug = false diff --git a/helm/ocaml/utf8_macros/pa_unicode_macro.ml b/helm/ocaml/utf8_macros/pa_unicode_macro.ml index d14401f84..dda7d4cab 100644 --- a/helm/ocaml/utf8_macros/pa_unicode_macro.ml +++ b/helm/ocaml/utf8_macros/pa_unicode_macro.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) diff --git a/helm/ocaml/utf8_macros/test.ml b/helm/ocaml/utf8_macros/test.ml index 7e1a48373..8f98bfd44 100644 --- a/helm/ocaml/utf8_macros/test.ml +++ b/helm/ocaml/utf8_macros/test.ml @@ -1 +1,3 @@ +(* $Id$ *) + prerr_endline <:unicode> diff --git a/helm/ocaml/utf8_macros/utf8Macro.ml b/helm/ocaml/utf8_macros/utf8Macro.ml index 3d0b5bc4c..e5fca10c4 100644 --- a/helm/ocaml/utf8_macros/utf8Macro.ml +++ b/helm/ocaml/utf8_macros/utf8Macro.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + exception Macro_not_found of string exception Utf8_not_found of string diff --git a/helm/ocaml/whelp/fwdQueries.ml b/helm/ocaml/whelp/fwdQueries.ml index 4e056b6b0..1f4e508fc 100644 --- a/helm/ocaml/whelp/fwdQueries.ml +++ b/helm/ocaml/whelp/fwdQueries.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + (* fwd_simpl ****************************************************************) let rec filter_map_n f n = function diff --git a/helm/ocaml/whelp/whelp.ml b/helm/ocaml/whelp/whelp.ml index d670b4372..5e63bcfc4 100644 --- a/helm/ocaml/whelp/whelp.ml +++ b/helm/ocaml/whelp/whelp.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf let nonvar uri = not (UriManager.uri_is_var uri) diff --git a/helm/ocaml/xml/test.ml b/helm/ocaml/xml/test.ml index 516ba77c6..84c042e28 100644 --- a/helm/ocaml/xml/test.ml +++ b/helm/ocaml/xml/test.ml @@ -1,3 +1,4 @@ +(* $Id$ *) (* Parsing test: * - XmlPushParser version *) diff --git a/helm/ocaml/xml/xml.ml b/helm/ocaml/xml/xml.ml index 809e11d3f..f8cc41cbe 100644 --- a/helm/ocaml/xml/xml.ml +++ b/helm/ocaml/xml/xml.ml @@ -36,6 +36,8 @@ (* *) (******************************************************************************) +(* $Id$ *) + (* the type token for XML cdata, empty elements and not-empty elements *) (* Usage: *) diff --git a/helm/ocaml/xml/xmlPushParser.ml b/helm/ocaml/xml/xmlPushParser.ml index 6cab0ead3..4f57e1242 100644 --- a/helm/ocaml/xml/xmlPushParser.ml +++ b/helm/ocaml/xml/xmlPushParser.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + let gzip_bufsize = 10240 type callbacks = { diff --git a/helm/ocaml/xmldiff/xmlDiff.ml b/helm/ocaml/xmldiff/xmlDiff.ml index c3a35ad34..6f68438e9 100644 --- a/helm/ocaml/xmldiff/xmlDiff.ml +++ b/helm/ocaml/xmldiff/xmlDiff.ml @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +(* $Id$ *) + let mathmlns = "http://www.w3.org/1998/Math/MathML";; let xmldiffns = "http://helm.cs.unibo.it/XmlDiff";; let helmns = "http://www.cs.unibo.it/helm";; -- 2.39.2