From: Claudio Sacerdoti Coen Date: Tue, 7 Jul 2009 01:49:29 +0000 (+0000) Subject: 1) Include files for NG were neither recursively processes nor accumulated. X-Git-Tag: make_still_working~3746 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a7237500e8a2a4237a6ae8ba4b8301f7bbcb6acb;p=helm.git 1) Include files for NG were neither recursively processes nor accumulated. They are now recursively processed (is this the best solution???) 2) Bug fixed (an assertion raised in including an included file because of a false assertion on references) --- diff --git a/helm/software/components/acic_content/.depend b/helm/software/components/acic_content/.depend index 8ade458af..89dca0e44 100644 --- a/helm/software/components/acic_content/.depend +++ b/helm/software/components/acic_content/.depend @@ -1,3 +1,4 @@ +content.cmi: acic2content.cmi: content.cmi content2cic.cmi: content.cmi cicNotationUtil.cmi: cicNotationPt.cmo @@ -5,6 +6,8 @@ cicNotationEnv.cmi: cicNotationPt.cmo cicNotationPp.cmi: cicNotationPt.cmo cicNotationEnv.cmi acic2astMatcher.cmi: cicNotationPt.cmo termAcicContent.cmi: cicNotationPt.cmo +cicNotationPt.cmo: +cicNotationPt.cmx: content.cmo: content.cmi content.cmx: content.cmi acic2content.cmo: content.cmi acic2content.cmi diff --git a/helm/software/components/acic_procedural/.depend b/helm/software/components/acic_procedural/.depend index 8d0128744..97238c4d8 100644 --- a/helm/software/components/acic_procedural/.depend +++ b/helm/software/components/acic_procedural/.depend @@ -1,6 +1,13 @@ +proceduralHelpers.cmi: +proceduralClassify.cmi: +proceduralOptimizer.cmi: +proceduralTypes.cmi: +proceduralMode.cmi: +proceduralConversion.cmi: procedural1.cmi: proceduralTypes.cmi procedural2.cmi: proceduralTypes.cmi proceduralTeX.cmi: proceduralTypes.cmi +acic2Procedural.cmi: proceduralHelpers.cmo: proceduralHelpers.cmi proceduralHelpers.cmx: proceduralHelpers.cmi proceduralClassify.cmo: proceduralHelpers.cmi proceduralClassify.cmi diff --git a/helm/software/components/binaries/extractor/.depend b/helm/software/components/binaries/extractor/.depend index e69de29bb..0c39328ae 100644 --- a/helm/software/components/binaries/extractor/.depend +++ b/helm/software/components/binaries/extractor/.depend @@ -0,0 +1,4 @@ +extractor.cmo: +extractor.cmx: +extractor_manager.cmo: +extractor_manager.cmx: diff --git a/helm/software/components/binaries/table_creator/.depend b/helm/software/components/binaries/table_creator/.depend index e69de29bb..33147b949 100644 --- a/helm/software/components/binaries/table_creator/.depend +++ b/helm/software/components/binaries/table_creator/.depend @@ -0,0 +1,2 @@ +table_creator.cmo: +table_creator.cmx: diff --git a/helm/software/components/binaries/transcript/.depend.opt b/helm/software/components/binaries/transcript/.depend.opt index efadc681e..f17459162 100644 --- a/helm/software/components/binaries/transcript/.depend.opt +++ b/helm/software/components/binaries/transcript/.depend.opt @@ -1,6 +1,11 @@ gallina8Parser.cmi: types.cmx grafiteParser.cmi: types.cmx grafite.cmi: types.cmx +engine.cmi: +types.cmo: +types.cmx: +options.cmo: +options.cmx: gallina8Parser.cmo: types.cmx options.cmx gallina8Parser.cmi gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi gallina8Lexer.cmo: options.cmx gallina8Parser.cmi diff --git a/helm/software/components/binaries/transcript/grafite.ml b/helm/software/components/binaries/transcript/grafite.ml index cae0bdfb5..d44a17c58 100644 --- a/helm/software/components/binaries/transcript/grafite.ml +++ b/helm/software/components/binaries/transcript/grafite.ml @@ -76,7 +76,7 @@ let command_of_macro macro = G.Executable (floc, G.Macro (floc, macro)) let require moo value = - command_of_obj (G.Include (floc, moo, value ^ ".ma")) + command_of_obj (G.Include (floc, moo, `OldAndNew, value ^ ".ma")) let coercion value = command_of_obj (G.Coercion (floc, UM.uri_of_string value, true, 0, 0)) diff --git a/helm/software/components/cic/.depend b/helm/software/components/cic/.depend index c2c7105c7..a835b247f 100644 --- a/helm/software/components/cic/.depend +++ b/helm/software/components/cic/.depend @@ -1,8 +1,10 @@ +cicUniv.cmi: unshare.cmi: cic.cmo deannotate.cmi: cic.cmo cicParser.cmi: cic.cmo cicUtil.cmi: cic.cmo helmLibraryObjects.cmi: cic.cmo +libraryObjects.cmi: cic_indexable.cmi: cic.cmo path_indexing.cmi: cic.cmo cicInspect.cmi: cic.cmo diff --git a/helm/software/components/cic_acic/.depend b/helm/software/components/cic_acic/.depend index 3fc1e0dce..5449d50aa 100644 --- a/helm/software/components/cic_acic/.depend +++ b/helm/software/components/cic_acic/.depend @@ -1,3 +1,6 @@ +eta_fixing.cmi: +doubleTypeInference.cmi: +cic2acic.cmi: cic2Xml.cmi: cic2acic.cmi eta_fixing.cmo: eta_fixing.cmi eta_fixing.cmx: eta_fixing.cmi diff --git a/helm/software/components/cic_disambiguation/.depend b/helm/software/components/cic_disambiguation/.depend index e9bd1168f..a9ae65a5e 100644 --- a/helm/software/components/cic_disambiguation/.depend +++ b/helm/software/components/cic_disambiguation/.depend @@ -1,3 +1,5 @@ +cicDisambiguate.cmi: +disambiguateChoices.cmi: cicDisambiguate.cmo: cicDisambiguate.cmi cicDisambiguate.cmx: cicDisambiguate.cmi disambiguateChoices.cmo: disambiguateChoices.cmi diff --git a/helm/software/components/cic_exportation/.depend b/helm/software/components/cic_exportation/.depend index 288ea5f6c..91be8d88d 100644 --- a/helm/software/components/cic_exportation/.depend +++ b/helm/software/components/cic_exportation/.depend @@ -1,2 +1,3 @@ +cicExportation.cmi: cicExportation.cmo: cicExportation.cmi cicExportation.cmx: cicExportation.cmi diff --git a/helm/software/components/cic_proof_checking/.depend b/helm/software/components/cic_proof_checking/.depend index 5d83fd0f3..f8a16629e 100644 --- a/helm/software/components/cic_proof_checking/.depend +++ b/helm/software/components/cic_proof_checking/.depend @@ -1,3 +1,13 @@ +cicLogger.cmi: +cicEnvironment.cmi: +cicPp.cmi: +cicUnivUtils.cmi: +cicSubstitution.cmi: +cicMiniReduction.cmi: +cicReduction.cmi: +cicTypeChecker.cmi: +freshNamesGenerator.cmi: +cicDischarge.cmi: cicLogger.cmo: cicLogger.cmi cicLogger.cmx: cicLogger.cmi cicEnvironment.cmo: cicEnvironment.cmi diff --git a/helm/software/components/cic_unification/.depend b/helm/software/components/cic_unification/.depend index a7b23ceb4..2e054f73d 100644 --- a/helm/software/components/cic_unification/.depend +++ b/helm/software/components/cic_unification/.depend @@ -1,3 +1,10 @@ +cicMetaSubst.cmi: +cicMkImplicit.cmi: +termUtil.cmi: +coercGraph.cmi: +cicUnification.cmi: +cicReplace.cmi: +cicRefine.cmi: cicMetaSubst.cmo: cicMetaSubst.cmi cicMetaSubst.cmx: cicMetaSubst.cmi cicMkImplicit.cmo: cicMkImplicit.cmi diff --git a/helm/software/components/content_pres/.depend b/helm/software/components/content_pres/.depend index 6dd0e78a1..8d74439eb 100644 --- a/helm/software/components/content_pres/.depend +++ b/helm/software/components/content_pres/.depend @@ -1,3 +1,9 @@ +renderingAttrs.cmi: +cicNotationLexer.cmi: +cicNotationParser.cmi: +mpresentation.cmi: +box.cmi: +content2presMatcher.cmi: termContentPres.cmi: cicNotationParser.cmi boxPp.cmi: mpresentation.cmi cicNotationPres.cmi box.cmi cicNotationPres.cmi: mpresentation.cmi box.cmi diff --git a/helm/software/components/disambiguation/.depend b/helm/software/components/disambiguation/.depend index aba9ffea7..9fdbeeeaf 100644 --- a/helm/software/components/disambiguation/.depend +++ b/helm/software/components/disambiguation/.depend @@ -1,3 +1,4 @@ +disambiguateTypes.cmi: disambiguate.cmi: disambiguateTypes.cmi multiPassDisambiguator.cmi: disambiguateTypes.cmi disambiguate.cmi disambiguateTypes.cmo: disambiguateTypes.cmi diff --git a/helm/software/components/extlib/.depend b/helm/software/components/extlib/.depend index 201cd0cba..dcc6377a0 100644 --- a/helm/software/components/extlib/.depend +++ b/helm/software/components/extlib/.depend @@ -1,3 +1,13 @@ +componentsConf.cmi: +hExtlib.cmi: +hMarshal.cmi: +patternMatcher.cmi: +hLog.cmi: +trie.cmi: +discrimination_tree.cmi: +hTopoSort.cmi: +refCounter.cmi: +graphvizPp.cmi: componentsConf.cmo: componentsConf.cmi componentsConf.cmx: componentsConf.cmi hExtlib.cmo: hExtlib.cmi diff --git a/helm/software/components/getter/.depend b/helm/software/components/getter/.depend index 20f69cf0c..ca64d8ec0 100644 --- a/helm/software/components/getter/.depend +++ b/helm/software/components/getter/.depend @@ -1,6 +1,13 @@ +http_getter_wget.cmi: +http_getter_logger.cmi: +http_getter_misc.cmi: +http_getter_const.cmi: http_getter_env.cmi: http_getter_types.cmo +http_getter_storage.cmi: http_getter_common.cmi: http_getter_types.cmo http_getter.cmi: http_getter_types.cmo +http_getter_types.cmo: +http_getter_types.cmx: http_getter_wget.cmo: http_getter_types.cmo http_getter_wget.cmi http_getter_wget.cmx: http_getter_types.cmx http_getter_wget.cmi http_getter_logger.cmo: http_getter_logger.cmi diff --git a/helm/software/components/grafite/.depend b/helm/software/components/grafite/.depend index dc225e221..f305b1580 100644 --- a/helm/software/components/grafite/.depend +++ b/helm/software/components/grafite/.depend @@ -1,5 +1,7 @@ grafiteAstPp.cmi: grafiteAst.cmo grafiteMarshal.cmi: grafiteAst.cmo +grafiteAst.cmo: +grafiteAst.cmx: grafiteAstPp.cmo: grafiteAst.cmo grafiteAstPp.cmi grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi grafiteMarshal.cmo: grafiteAstPp.cmi grafiteAst.cmo grafiteMarshal.cmi diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 524f99dc2..e807c6f48 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -188,7 +188,7 @@ type ('term,'lazy_term) macro = (** To be increased each time the command type below changes, used for "safe" * marshalling *) -let magic = 24 +let magic = 25 type ('term,'obj) command = | Index of loc * 'term option (* key *) * UriManager.uri (* value *) @@ -200,7 +200,7 @@ type ('term,'obj) command = | Inverter of loc * string * 'term * bool list | Default of loc * string * UriManager.uri list | Drop of loc - | Include of loc * bool (* normal? *) * string + | Include of loc * bool (* normal? *) * [`New | `OldAndNew] * string | Obj of loc * 'obj | Relation of loc * string * 'term * 'term * 'term option * 'term option * 'term option diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 7ececab72..f05cb9595 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -370,8 +370,9 @@ let pp_command ~term_pp ~obj_pp = function "inverter " ^ n ^ " for " ^ term_pp ty ^ " " ^ List.fold_left (fun acc x -> acc ^ (match x with true -> "%" | _ -> "?")) "" params | Default (_,what,uris) -> pp_default what uris | Drop _ -> "drop" - | Include (_,true,path) -> "include \"" ^ path ^ "\"" - | Include (_,false,path) -> "include source \"" ^ path ^ "\"" + | Include (_,true,`OldAndNew,path) -> "include \"" ^ path ^ "\"" + | Include (_,false,`OldAndNew,path) -> "include source \"" ^ path ^ "\"" + | Include (_,_,`New,path) -> "RECURSIVELY INCLUDING " ^ path | Obj (_,obj) -> obj_pp obj | Qed _ -> "qed" | Relation (_,id,a,aeq,refl,sym,trans) -> diff --git a/helm/software/components/grafite/grafiteMarshal.ml b/helm/software/components/grafite/grafiteMarshal.ml index 481a1b21d..d666f62b6 100644 --- a/helm/software/components/grafite/grafiteMarshal.ml +++ b/helm/software/components/grafite/grafiteMarshal.ml @@ -52,6 +52,7 @@ let rehash_cmd_uris = GrafiteAst.Index (loc, HExtlib.map_option CicUtil.rehash_term key, rehash_uri uri) | GrafiteAst.Select (loc, uri) -> GrafiteAst.Select (loc, rehash_uri uri) + | GrafiteAst.Include _ as cmd -> cmd | cmd -> prerr_endline "Found a command not expected in a .moo:"; let term_pp _ = assert false in diff --git a/helm/software/components/grafite_engine/.depend b/helm/software/components/grafite_engine/.depend index b0d4b7048..2dca47091 100644 --- a/helm/software/components/grafite_engine/.depend +++ b/helm/software/components/grafite_engine/.depend @@ -1,3 +1,4 @@ +grafiteTypes.cmi: grafiteSync.cmi: grafiteTypes.cmi grafiteEngine.cmi: grafiteTypes.cmi grafiteTypes.cmo: grafiteTypes.cmi diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 5d1ea5096..9817474cd 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -820,24 +820,32 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status LibraryObjects.set_default what uris; GrafiteTypes.add_moo_content [cmd] status,`Old [] | GrafiteAst.Drop loc -> raise Drop - | GrafiteAst.Include (loc, _, baseuri) -> - let moopath_rw, moopath_r = - LibraryMisc.obj_file_of_baseuri - ~must_exist:false ~baseuri ~writable:true, - LibraryMisc.obj_file_of_baseuri - ~must_exist:false ~baseuri ~writable:false - in - let moopath = - if Sys.file_exists moopath_r then moopath_r else - if Sys.file_exists moopath_rw then moopath_rw else - raise (IncludedFileNotCompiled (moopath_rw,baseuri)) - in - let status = eval_from_moo.efm_go status moopath in + | GrafiteAst.Include (loc, mode, new_or_old, baseuri) -> + (* Old Include command is not recursive; new one is *) let status = - NRstatus.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) - status + if new_or_old = `OldAndNew then + let moopath_rw, moopath_r = + LibraryMisc.obj_file_of_baseuri + ~must_exist:false ~baseuri ~writable:true, + LibraryMisc.obj_file_of_baseuri + ~must_exist:false ~baseuri ~writable:false in + let moopath = + if Sys.file_exists moopath_r then moopath_r else + if Sys.file_exists moopath_rw then moopath_rw else + raise (IncludedFileNotCompiled (moopath_rw,baseuri)) + in + eval_from_moo.efm_go status moopath + else + status in - status,`Old [] + let status = + NRstatus.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) + status in + let status = + GrafiteTypes.add_moo_content + [GrafiteAst.Include (loc,mode,`New,baseuri)] status + in + status,`Old [] | GrafiteAst.Print (_,"proofterm") -> let _,_,_,p,_, _ = GrafiteTypes.get_current_proof status in prerr_endline (Auto.pp_proofterm (Lazy.force p)); diff --git a/helm/software/components/grafite_parser/.depend b/helm/software/components/grafite_parser/.depend index 97bf4d7c2..2766b04d0 100644 --- a/helm/software/components/grafite_parser/.depend +++ b/helm/software/components/grafite_parser/.depend @@ -1,4 +1,9 @@ +dependenciesParser.cmi: +grafiteParser.cmi: +cicNotation2.cmi: +nEstatus.cmi: grafiteDisambiguate.cmi: nEstatus.cmi +print_grammar.cmi: dependenciesParser.cmo: dependenciesParser.cmi dependenciesParser.cmx: dependenciesParser.cmi grafiteParser.cmo: grafiteParser.cmi diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 481d49f08..cc2bf2cda 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -949,21 +949,23 @@ EXTEND status, LSome stm | (iloc,fname,normal,mode) = include_command ; SYMBOL "." -> fun ?(never_include=false) ~include_paths status -> + let _root, buri, fullpath, _rrelpath = + Librarian.baseuri_of_script ~include_paths fname in + if never_include then raise (NoInclusionPerformed fullpath) + else + begin let stm = - G.Executable (loc, G.Command (loc, G.Include (iloc, normal, fname))) - in + G.Executable + (loc, G.Command (loc, G.Include (iloc,normal,`OldAndNew,fname))) in !grafite_callback stm; - let _root, buri, fullpath, _rrelpath = - Librarian.baseuri_of_script ~include_paths fname - in let status = - if never_include then raise (NoInclusionPerformed fullpath) - else LE.eval_command status (L.Include (iloc,buri,mode,fullpath)) - in + LE.eval_command status (L.Include (iloc,buri,mode,fullpath)) in let stm = - G.Executable (loc, G.Command (loc, G.Include (iloc, normal, buri))) + G.Executable + (loc,G.Command (loc,G.Include (iloc,normal,`OldAndNew,buri))) in - status, LSome stm + status, LSome stm + end | scom = lexicon_command ; SYMBOL "." -> fun ?(never_include=false) ~include_paths status -> !lexicon_callback scom; diff --git a/helm/software/components/hgdome/.depend b/helm/software/components/hgdome/.depend index bf9c09af7..072d9697a 100644 --- a/helm/software/components/hgdome/.depend +++ b/helm/software/components/hgdome/.depend @@ -1,3 +1,5 @@ +domMisc.cmi: +xml2Gdome.cmi: domMisc.cmo: domMisc.cmi domMisc.cmx: domMisc.cmi xml2Gdome.cmo: xml2Gdome.cmi diff --git a/helm/software/components/hmysql/.depend b/helm/software/components/hmysql/.depend index 16e6e9da7..ce439d961 100644 --- a/helm/software/components/hmysql/.depend +++ b/helm/software/components/hmysql/.depend @@ -1,2 +1,7 @@ +hSql.cmi: +hSqlite3.cmo: +hSqlite3.cmx: +hMysql.cmo: +hMysql.cmx: hSql.cmo: hSqlite3.cmo hMysql.cmo hSql.cmi hSql.cmx: hSqlite3.cmx hMysql.cmx hSql.cmi diff --git a/helm/software/components/lexicon/.depend b/helm/software/components/lexicon/.depend index 847a4a807..16c114516 100644 --- a/helm/software/components/lexicon/.depend +++ b/helm/software/components/lexicon/.depend @@ -3,6 +3,8 @@ lexiconMarshal.cmi: lexiconAst.cmo cicNotation.cmi: lexiconAst.cmo lexiconEngine.cmi: lexiconMarshal.cmi lexiconAst.cmo cicNotation.cmi lexiconSync.cmi: lexiconEngine.cmi lexiconAst.cmo +lexiconAst.cmo: +lexiconAst.cmx: lexiconAstPp.cmo: lexiconAst.cmo lexiconAstPp.cmi lexiconAstPp.cmx: lexiconAst.cmx lexiconAstPp.cmi lexiconMarshal.cmo: lexiconAstPp.cmi lexiconAst.cmo lexiconMarshal.cmi diff --git a/helm/software/components/lexicon/lexiconMarshal.ml b/helm/software/components/lexicon/lexiconMarshal.ml index ba7e583d5..5d69fafc0 100644 --- a/helm/software/components/lexicon/lexiconMarshal.ml +++ b/helm/software/components/lexicon/lexiconMarshal.ml @@ -45,7 +45,9 @@ let rehash_cmd_uris = function | CicNotationPt.UriPattern uri -> CicNotationPt.UriPattern (rehash_uri uri) - | CicNotationPt.NRefPattern _ -> assert false + | CicNotationPt.NRefPattern (NReference.Ref (uri,spec)) -> + let uri = NCicLibrary.refresh_uri uri in + CicNotationPt.NRefPattern (NReference.reference_of_spec uri spec) | CicNotationPt.ApplPattern args -> CicNotationPt.ApplPattern (List.map aux args) | CicNotationPt.VarPattern _ diff --git a/helm/software/components/library/.depend b/helm/software/components/library/.depend index a9f24f814..cfa1295ed 100644 --- a/helm/software/components/library/.depend +++ b/helm/software/components/library/.depend @@ -1,4 +1,13 @@ +librarian.cmi: +libraryMisc.cmi: +libraryDb.cmi: +coercDb.cmi: cicCoercion.cmi: coercDb.cmi +librarySync.cmi: +cicElim.cmi: +cicRecord.cmi: +cicFix.cmi: +libraryClean.cmi: librarian.cmo: librarian.cmi librarian.cmx: librarian.cmi libraryMisc.cmo: libraryMisc.cmi diff --git a/helm/software/components/logger/.depend b/helm/software/components/logger/.depend index 28268d29e..dfb4400ff 100644 --- a/helm/software/components/logger/.depend +++ b/helm/software/components/logger/.depend @@ -1,2 +1,3 @@ +helmLogger.cmi: helmLogger.cmo: helmLogger.cmi helmLogger.cmx: helmLogger.cmi diff --git a/helm/software/components/metadata/.depend b/helm/software/components/metadata/.depend index 492a34e3a..78cd97a0d 100644 --- a/helm/software/components/metadata/.depend +++ b/helm/software/components/metadata/.depend @@ -1,3 +1,5 @@ +sqlStatements.cmi: +metadataTypes.cmi: metadataExtractor.cmi: metadataTypes.cmi metadataPp.cmi: metadataTypes.cmi metadataConstraints.cmi: metadataTypes.cmi diff --git a/helm/software/components/ng_cic_content/.depend b/helm/software/components/ng_cic_content/.depend index b4e17fa99..1316c8eab 100644 --- a/helm/software/components/ng_cic_content/.depend +++ b/helm/software/components/ng_cic_content/.depend @@ -1,3 +1,5 @@ +ncic2astMatcher.cmi: +nTermCicContent.cmi: ncic2astMatcher.cmo: ncic2astMatcher.cmi ncic2astMatcher.cmx: ncic2astMatcher.cmi nTermCicContent.cmo: ncic2astMatcher.cmi nTermCicContent.cmi diff --git a/helm/software/components/ng_disambiguation/.depend b/helm/software/components/ng_disambiguation/.depend index 6b4ef95c1..2de54dc5e 100644 --- a/helm/software/components/ng_disambiguation/.depend +++ b/helm/software/components/ng_disambiguation/.depend @@ -1,2 +1,3 @@ +nCicDisambiguate.cmi: nCicDisambiguate.cmo: nCicDisambiguate.cmi nCicDisambiguate.cmx: nCicDisambiguate.cmi diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend index 4b11d9af6..a41138342 100644 --- a/helm/software/components/ng_kernel/.depend +++ b/helm/software/components/ng_kernel/.depend @@ -1,3 +1,4 @@ +nUri.cmi: nReference.cmi: nUri.cmi nCicUtils.cmi: nCic.cmo nCicSubstitution.cmi: nCic.cmo diff --git a/helm/software/components/ng_kernel/nCicLibrary.mli b/helm/software/components/ng_kernel/nCicLibrary.mli index 30dcc263c..2911204ae 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.mli +++ b/helm/software/components/ng_kernel/nCicLibrary.mli @@ -52,4 +52,7 @@ module Serializer(S: sig type status end): Serializer with type status= S.status val init: unit -> unit +(* CSC: only required during old-to-NG phase, to be deleted *) +val refresh_uri: NUri.uri -> NUri.uri + (* EOF *) diff --git a/helm/software/components/ng_paramodulation/.depend b/helm/software/components/ng_paramodulation/.depend index b78122fff..1b07492f1 100644 --- a/helm/software/components/ng_paramodulation/.depend +++ b/helm/software/components/ng_paramodulation/.depend @@ -1,3 +1,4 @@ +terms.cmi: pp.cmi: terms.cmi foSubst.cmi: terms.cmi orderings.cmi: terms.cmi @@ -9,6 +10,7 @@ paramod.cmi: terms.cmi nCicBlob.cmi: terms.cmi cicBlob.cmi: terms.cmi nCicProof.cmi: terms.cmi +nCicParamod.cmi: terms.cmo: terms.cmi terms.cmx: terms.cmi pp.cmo: terms.cmi pp.cmi @@ -27,10 +29,10 @@ superposition.cmo: terms.cmi pp.cmi orderings.cmi index.cmi foUtils.cmi \ foUnif.cmi foSubst.cmi superposition.cmi superposition.cmx: terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \ foUnif.cmx foSubst.cmx superposition.cmi -paramod.cmo: terms.cmi superposition.cmi pp.cmi index.cmi foUtils.cmi \ - foUnif.cmi paramod.cmi -paramod.cmx: terms.cmx superposition.cmx pp.cmx index.cmx foUtils.cmx \ - foUnif.cmx paramod.cmi +paramod.cmo: terms.cmi superposition.cmi pp.cmi orderings.cmi index.cmi \ + foUtils.cmi foUnif.cmi paramod.cmi +paramod.cmx: terms.cmx superposition.cmx pp.cmx orderings.cmx index.cmx \ + foUtils.cmx foUnif.cmx paramod.cmi nCicBlob.cmo: terms.cmi foUtils.cmi nCicBlob.cmi nCicBlob.cmx: terms.cmx foUtils.cmx nCicBlob.cmi cicBlob.cmo: terms.cmi cicBlob.cmi diff --git a/helm/software/components/ng_refiner/.depend b/helm/software/components/ng_refiner/.depend index 1f93f1327..924b43fe8 100644 --- a/helm/software/components/ng_refiner/.depend +++ b/helm/software/components/ng_refiner/.depend @@ -1,3 +1,7 @@ +nDiscriminationTree.cmi: +nCicMetaSubst.cmi: +nCicCoercion.cmi: +nCicUnifHint.cmi: nRstatus.cmi: nCicUnifHint.cmi nCicCoercion.cmi nCicUnification.cmi: nRstatus.cmi nCicRefiner.cmi: nRstatus.cmi diff --git a/helm/software/components/ng_tactics/.depend b/helm/software/components/ng_tactics/.depend index 3ce24c446..636e38f58 100644 --- a/helm/software/components/ng_tactics/.depend +++ b/helm/software/components/ng_tactics/.depend @@ -1,4 +1,7 @@ +nCicTacReduction.cmi: +nTacStatus.cmi: nTactics.cmi: nTacStatus.cmi +nCicElim.cmi: nCicTacReduction.cmo: nCicTacReduction.cmi nCicTacReduction.cmx: nCicTacReduction.cmi nTacStatus.cmo: nCicTacReduction.cmi nTacStatus.cmi diff --git a/helm/software/components/registry/.depend b/helm/software/components/registry/.depend index cf4f36b68..40c03891a 100644 --- a/helm/software/components/registry/.depend +++ b/helm/software/components/registry/.depend @@ -1,2 +1,3 @@ +helm_registry.cmi: helm_registry.cmo: helm_registry.cmi helm_registry.cmx: helm_registry.cmi diff --git a/helm/software/components/tactics/.depend b/helm/software/components/tactics/.depend index 169fc76b0..d9d6034a1 100644 --- a/helm/software/components/tactics/.depend +++ b/helm/software/components/tactics/.depend @@ -1,11 +1,19 @@ +proofEngineTypes.cmi: proofEngineHelpers.cmi: proofEngineTypes.cmi +proofEngineReduction.cmi: continuationals.cmi: proofEngineTypes.cmi tacticals.cmi: proofEngineTypes.cmi reductionTactics.cmi: proofEngineTypes.cmi proofEngineStructuralRules.cmi: proofEngineTypes.cmi primitiveTactics.cmi: proofEngineTypes.cmi +hashtbl_equiv.cmi: metadataQuery.cmi: proofEngineTypes.cmi +universe.cmi: autoTypes.cmi: proofEngineTypes.cmi +autoCache.cmi: +paramodulation/utils.cmi: +closeCoercionGraph.cmi: +paramodulation/subst.cmi: paramodulation/equality.cmi: paramodulation/utils.cmi \ paramodulation/subst.cmi paramodulation/founif.cmi: paramodulation/subst.cmi @@ -27,10 +35,13 @@ equalityTactics.cmi: proofEngineTypes.cmi auto.cmi: proofEngineTypes.cmi automationCache.cmi destructTactic.cmi: proofEngineTypes.cmi inversion.cmi: proofEngineTypes.cmi +inversion_principle.cmi: ring.cmi: proofEngineTypes.cmi setoids.cmi: proofEngineTypes.cmi +fourier.cmi: fourierR.cmi: proofEngineTypes.cmi fwdSimplTactic.cmi: proofEngineTypes.cmi +history.cmi: statefulProofEngine.cmi: proofEngineTypes.cmi tactics.cmi: tacticals.cmi proofEngineTypes.cmi automationCache.cmi auto.cmi declarative.cmi: proofEngineTypes.cmi automationCache.cmi auto.cmi diff --git a/helm/software/components/thread/.depend b/helm/software/components/thread/.depend index 7759190c6..6616a03d0 100644 --- a/helm/software/components/thread/.depend +++ b/helm/software/components/thread/.depend @@ -1,3 +1,5 @@ +threadSafe.cmi: +extThread.cmi: threadSafe.cmo: threadSafe.cmi threadSafe.cmx: threadSafe.cmi extThread.cmo: extThread.cmi diff --git a/helm/software/components/tptp_grafite/.depend b/helm/software/components/tptp_grafite/.depend index bc310327f..a8972f4cf 100644 --- a/helm/software/components/tptp_grafite/.depend +++ b/helm/software/components/tptp_grafite/.depend @@ -1,4 +1,7 @@ parser.cmi: ast.cmo +tptp2grafite.cmi: +ast.cmo: +ast.cmx: lexer.cmo: parser.cmi lexer.cmx: parser.cmx parser.cmo: ast.cmo parser.cmi diff --git a/helm/software/components/tptp_grafite/tptp2grafite.ml b/helm/software/components/tptp_grafite/tptp2grafite.ml index 009a53a61..a19fa67c2 100644 --- a/helm/software/components/tptp_grafite/tptp2grafite.ml +++ b/helm/software/components/tptp_grafite/tptp2grafite.ml @@ -440,8 +440,9 @@ let tptp2grafite ?(timeout=600) ?(def_depth=10) ?raw_preamble ~tptppath ~filenam let preamble = match raw_preamble with | None -> - pp (GA.Executable(floc, - GA.Command(floc,GA.Include(floc,true,"logic/equality.ma")))) + pp + (GA.Executable(floc, + GA.Command(floc,GA.Include(floc,true,`OldAndNew,"logic/equality.ma")))) | Some s -> s buri in let extra_statements_end = [] in diff --git a/helm/software/components/urimanager/.depend b/helm/software/components/urimanager/.depend index 482148423..9cac9aa78 100644 --- a/helm/software/components/urimanager/.depend +++ b/helm/software/components/urimanager/.depend @@ -1,2 +1,3 @@ +uriManager.cmi: uriManager.cmo: uriManager.cmi uriManager.cmx: uriManager.cmi diff --git a/helm/software/components/whelp/.depend b/helm/software/components/whelp/.depend index 39f37dfa9..65dc07955 100644 --- a/helm/software/components/whelp/.depend +++ b/helm/software/components/whelp/.depend @@ -1,3 +1,5 @@ +whelp.cmi: +fwdQueries.cmi: whelp.cmo: whelp.cmi whelp.cmx: whelp.cmi fwdQueries.cmo: fwdQueries.cmi diff --git a/helm/software/components/xml/.depend b/helm/software/components/xml/.depend index 5ef59bdc9..e7e7ffbd7 100644 --- a/helm/software/components/xml/.depend +++ b/helm/software/components/xml/.depend @@ -1,3 +1,5 @@ +xml.cmi: +xmlPushParser.cmi: xml.cmo: xml.cmi xml.cmx: xml.cmi xmlPushParser.cmo: xmlPushParser.cmi diff --git a/helm/software/components/xmldiff/.depend b/helm/software/components/xmldiff/.depend index e2832de33..65bd7b949 100644 --- a/helm/software/components/xmldiff/.depend +++ b/helm/software/components/xmldiff/.depend @@ -1,2 +1,3 @@ +xmlDiff.cmi: xmlDiff.cmo: xmlDiff.cmi xmlDiff.cmx: xmlDiff.cmi diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index 36f7cda6d..2c5160572 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/matita/matitacLib.ml @@ -77,7 +77,7 @@ let dump f = (Helm_registry.get_bool "matita.paste_unicode_as_tex") in output_string och str - | G.Executable (loc, G.Command (_, G.Include (_, false, _))) -> () + | G.Executable (loc, G.Command (_, G.Include (_, false, _, _))) -> () | stm -> output_string och (pp_statement stm); nl (); nl () in