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 8ade458af771b340426f4e4606d92e511c459a56..89dca0e446d48d1f05a1cda5fc3c39f1095257e3 100644 (file)
--- 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 8d0128744c8b9e740462a1a8001764036199a67e..97238c4d861fc8ee80cbafc6c9c6337d3e3babf2 100644 (file)
--- 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 e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0c39328ae147e8ab714b2d3a7b1582a011b2b1d6 100644 (file)
--- 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 e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..33147b94948d28fc9c7132773964d2547472c2ba 100644 (file)
--- 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 efadc681eee16cb3cd170845fdd1c7549fbb89b0..f17459162ce81c0ad9c5352cca5e9d99f43cb81c 100644 (file)
--- 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 cae0bdfb53aef4aff69e27e4ff00c220a157e687..d44a17c5897e40df09508101d852b3025a0c060a 100644 (file)
--- 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 c2c7105c727f1c8101a1a119d3521629984d3dcf..a835b247f3b3006e53a73a62b9ff56d394eca590 100644 (file)
--- 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 3fc1e0dce9eedda1f0bb74a669ad175582f03e06..5449d50aaa2d43c1a8126f0561177e904f0975da 100644 (file)
--- 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 e9bd1168f73e4e834b02480bca0e67e381fc4997..a9ae65a5e3c4c3df2f8aaca3b2762c794bee6bd5 100644 (file)
--- 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 288ea5f6cf50f1cb6bb8ff00d53a0262825c3459..91be8d88d36bf6f3df5cd920db6a75f80a5ff64d 100644 (file)
--- 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 5d83fd0f3d146e2d80ead2d8eb5c34b162a5835f..f8a16629ebd091a0c9e60b948c7e2eedb8908a16 100644 (file)
--- 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 a7b23ceb4e8ba6ae3fdc2fa8352ce69acbde78b0..2e054f73d4e69376cc89138609538274bd8fe6d8 100644 (file)
--- 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 6dd0e78a19212937b664b03fb796d8aaf496dbbb..8d74439eb72834455b6f06006f1f5534312a3a51 100644 (file)
--- 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 aba9ffea7f8db60089a7cf1831da09dcf9d0c67d..9fdbeeeafa878cfe32dbf1f96adaad1e3044a4eb 100644 (file)
--- 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 201cd0cba99efc82def4f425a72ba0e952c1a5ea..dcc6377a0664b620f19f47d8103c5b3a88a03270 100644 (file)
--- 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 20f69cf0c810c91e600fa5263c93c1b0ce86f3cb..ca64d8ec04f2c9e9b431d4921064c88bbb7587c9 100644 (file)
--- 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 dc225e2212dc37bb6eb22aa150fddf713965a312..f305b15803a9f6b7f87ab353a1e871afb8f6a1a5 100644 (file)
--- 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 524f99dc2ff389356bb1de7b2f586f3cd3cf9a1e..e807c6f48eacca783e51be27210bb30cde4adc23 100644 (file)
--- 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 7ececab722b2b5ff61037ed76ea76df4c0276d81..f05cb9595b9bb9676b8631d8a6a941addb5af81c 100644 (file)
--- 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 481a1b21dcacaed45448da576d50378433d5d616..d666f62b61837163fe53dc9905fdc0d2f2df1020 100644 (file)
--- 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 b0d4b7048ba7d34ad668443037fa5c8cb6676fff..2dca47091ba6d7eb068e394a7f5b5cd02fcd83bf 100644 (file)
--- 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 5d1ea50962f211c333732ebc1fafb1622194b640..9817474cddbb50cadea0f5b143d333bb65fdc3ce 100644 (file)
--- 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 97bf4d7c26591b45c8b7710b18ccc7b10bfce265..2766b04d03ad96eb26664ce893da8d732191ede5 100644 (file)
--- 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 481d49f08db75716160add58d1d42958c41effef..cc2bf2cdac6d96cd98feff25951991af05ece7cb 100644 (file)
--- 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 bf9c09af77949af3443918acfe26309ababdde62..072d9697ac67fab4c4d0dffd6321082b1022c444 100644 (file)
--- 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 16e6e9da7ff478b574edcc5f5756da5ac302ed34..ce439d961c5806d62c02572a1790a6b6591aad1a 100644 (file)
--- 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 847a4a807733e1ff71a24f44d6ff3ed18dd0252b..16c1145165e3acf1c2c923e16a634ce3f3967bef 100644 (file)
--- 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 ba7e583d555c8eb882b1f994bf8ba5b0d4312052..5d69fafc002cd6751f69813d026720a068d3654a 100644 (file)
--- 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 a9f24f814f3dfb119e00e1fe2f6d71ef565d38ff..cfa1295edcd418319d423cb3ad3f4cc106a1ff21 100644 (file)
--- 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 28268d29ee15cd05d86a0565b7d47abfe8ecf81f..dfb4400ff0dce00c92943043edccecc0c1222ed5 100644 (file)
--- 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 492a34e3a9dad11aa9a08d4a09802647c6e0bf95..78cd97a0deff8787b73aed2878acef8374029ee0 100644 (file)
--- 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 b4e17fa99bca931a5289d06541f5b69060d11594..1316c8eab83e4c08ca7047ed72175492e98197a1 100644 (file)
--- 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 6b4ef95c1ee75472df6140057f1b06851033b996..2de54dc5eaedce21d8850cc5f76cc76f38331752 100644 (file)
--- 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 4b11d9af63b98c6343b5fcc70cb32931340bc6ad..a411383423165650cb5f7e49eb9b516d94989881 100644 (file)
--- 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 30dcc263c0d1c6afb3866bc30dbee11fb6049cb9..2911204ae50d0370375b56f4ac772e370a0952fb 100644 (file)
--- 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 b78122fff4b3432436603a190ad995f15543b76b..1b07492f13532026c7818bc2e8a4b27463189390 100644 (file)
--- 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 1f93f13272de28521ef99e4ca00a32e74cbc2633..924b43fe8b1e756cd613663bd3e09f5adf9fd7d8 100644 (file)
--- 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 3ce24c446494b9e6e9690f964366bd16736d9e4f..636e38f58846218d36165745ff52ee0387b83cd2 100644 (file)
--- 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 cf4f36b68f502fc728be91d4b20e8b0dcd3658f2..40c03891a7433c13e27e38dbe1cb51e06030c905 100644 (file)
--- 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 169fc76b0e21d9fad98c2fa23430aeb0fa3a0f81..d9d6034a11e090bef20f2d14ccd1d8fb4e5692e2 100644 (file)
--- 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 7759190c66cdd57bcc79c0da85a571cd76faa730..6616a03d0f4c0803fa1e9c2e309bbf89270e7526 100644 (file)
--- 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 bc310327f83551dd5875e62bfa3899e7c55559a2..a8972f4cfc20c049020440e4f567cfb622de8243 100644 (file)
--- 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 009a53a610686a0d352e5dce681f066372abdb79..a19fa67c20d3281967d8ec77a754f84ede510a51 100644 (file)
--- 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 4821484239ac15df403da8d9123671544b3aa65f..9cac9aa783c7c003e70e118017c77b20d2ccb61a 100644 (file)
--- 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 39f37dfa90077f1212c1f51f57ef8c55a21174c7..65dc079553f6476748ecdb106d61534fa746d753 100644 (file)
--- 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 5ef59bdc96d40e0a64e0f50d91b949382a7f57e0..e7e7ffbd729fcdbc6206eb38afebf53940878718 100644 (file)
--- 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 e2832de332dd83fb5bd4beb1cd2b1e735d6fe35e..65bd7b9496155f928775a264636cae0249c62a98 100644 (file)
--- 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 36f7cda6dc9d059bb22a14324dfbdd3febdc00f5..2c5160572f57e6f873a682d9efed6f7c0aaa9e20 100644 (file)
--- 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