- New attribute `Implied put beside `Generated and `Provided.

  It denotes an object provided not as defined by the user, but as generated by another ITP
  New optional keyword "implied" recognized in front of:
  theorem, definition, ..., let rec, let corec
  specifies to construct an object with this new attribute.
  [still not admitted in front of inductive, coinductive, record]

diff --git a/matita/components/binaries/probe/options.mli b/matita/components/binaries/probe/options.mli
index 3e9789c76f133457e216200e71fff75d3c463460..a692c90133b3d668fa3c57bb500b72f6f6122416 100644 (file)
--- a/matita/components/binaries/probe/options.mli
+++ b/matita/components/binaries/probe/options.mli
@@ -15,7 +15,7 @@ val srcs: NUri.UriSet.t ref
 
 val remove: string list ref
 
-val exclude: NCic.generated list ref
+val exclude: NCic.source list ref
 
 val net: int ref
 

diff --git a/matita/components/binaries/probe/probe.ml b/matita/components/binaries/probe/probe.ml
index 55b942cc10a2552bd5b2114f63c7ce4fdd7ac3ed..748826be167cf6b159ec5eff6aafbc3aa9a654c7 100644 (file)
--- a/matita/components/binaries/probe/probe.ml
+++ b/matita/components/binaries/probe/probe.ml
@@ -46,9 +46,11 @@ let scan_from devel =
 
 let set_g () = O.exclude := `Generated :: !O.exclude
 
+let set_i () = O.exclude := `Implied :: !O.exclude
+
 let set_p () = O.exclude := `Provided :: !O.exclude
 
-let out_i () = E.out_int !O.net
+let out_c () = E.out_int !O.net
 
 let out_on () = E.out_length !O.objs
 
@@ -67,10 +69,11 @@ let clear () =
    D.objects (); O.clear ()
 
 let _ =
-   let help = "Usage: probe [ -X | <configuration file> | -gp | HELM (base)uri | -i | -on | os | -sn | -ss  ]*" in
+   let help = "Usage: probe [ -X | <configuration file> | -gip | HELM (base)uri | -c | -on | os | -sn | -ss  ]*" in
    let help_X  = " Clear configuration, options and counters" in
+   let help_c  = " Print the total intrinsic complexity" in
    let help_g  = " Exclude generated objects" in
-   let help_i  = " Print the total intrinsic size" in
+   let help_i  = " Exclude implied objects" in
    let help_p  = " Exclude provided objects" in
    let help_on = " Print the number of objects" in
    let help_os = " Print the list of objects" in
@@ -78,8 +81,9 @@ let _ =
    let help_ss = " Print the list of sources" in
    A.parse [
       "-X" , A.Unit clear, help_X;
+      "-c" , A.Unit out_c, help_c;
       "-g" , A.Unit set_g, help_g;
-      "-i" , A.Unit out_i, help_i;
+      "-i" , A.Unit set_i, help_i;
       "-on", A.Unit out_on, help_on;
       "-os", A.Unit out_os, help_os;
       "-p" , A.Unit set_p, help_p;      

diff --git a/matita/components/content/.depend b/matita/components/content/.depend
index 0671b66fe9c5b8e4748c39e8b0176cc7322134ef..369dbbdc4e978ce0baf7408ca0779e8253557ac8 100644 (file)
--- a/matita/components/content/.depend
+++ b/matita/components/content/.depend
@@ -1,14 +1,14 @@
-content.cmi:
-notationUtil.cmi: notationPt.cmo
-notationEnv.cmi: notationPt.cmo
-notationPp.cmi: notationPt.cmo notationEnv.cmi
-notationPt.cmo:
-notationPt.cmx:
-content.cmo: content.cmi
-content.cmx: content.cmi
-notationUtil.cmo: notationPt.cmo notationUtil.cmi
-notationUtil.cmx: notationPt.cmx notationUtil.cmi
-notationEnv.cmo: notationUtil.cmi notationPt.cmo notationEnv.cmi
-notationEnv.cmx: notationUtil.cmx notationPt.cmx notationEnv.cmi
-notationPp.cmo: notationPt.cmo notationEnv.cmi notationPp.cmi
-notationPp.cmx: notationPt.cmx notationEnv.cmx notationPp.cmi
+content.cmi :
+notationUtil.cmi : notationPt.cmo
+notationEnv.cmi : notationPt.cmo
+notationPp.cmi : notationPt.cmo notationEnv.cmi
+notationPt.cmo :
+notationPt.cmx :
+content.cmo : content.cmi
+content.cmx : content.cmi
+notationUtil.cmo : notationPt.cmo notationUtil.cmi
+notationUtil.cmx : notationPt.cmx notationUtil.cmi
+notationEnv.cmo : notationUtil.cmi notationPt.cmo notationEnv.cmi
+notationEnv.cmx : notationUtil.cmx notationPt.cmx notationEnv.cmi
+notationPp.cmo : notationPt.cmo notationEnv.cmi notationPp.cmi
+notationPp.cmx : notationPt.cmx notationEnv.cmx notationPp.cmi

diff --git a/matita/components/content_pres/.depend b/matita/components/content_pres/.depend
index 03a1732eb9be3f3c8e2d1aeaebc618438c4433a0..4deb6e591a8c9b1118318f7a7264800d533fbece 100644 (file)
--- a/matita/components/content_pres/.depend
+++ b/matita/components/content_pres/.depend
@@ -1,38 +1,38 @@
-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
-content2pres.cmi: termContentPres.cmi cicNotationPres.cmi
-renderingAttrs.cmo: renderingAttrs.cmi
-renderingAttrs.cmx: renderingAttrs.cmi
-cicNotationLexer.cmo: cicNotationLexer.cmi
-cicNotationLexer.cmx: cicNotationLexer.cmi
-cicNotationParser.cmo: cicNotationLexer.cmi cicNotationParser.cmi
-cicNotationParser.cmx: cicNotationLexer.cmx cicNotationParser.cmi
-mpresentation.cmo: mpresentation.cmi
-mpresentation.cmx: mpresentation.cmi
-box.cmo: renderingAttrs.cmi box.cmi
-box.cmx: renderingAttrs.cmx box.cmi
-content2presMatcher.cmo: content2presMatcher.cmi
-content2presMatcher.cmx: content2presMatcher.cmi
-termContentPres.cmo: renderingAttrs.cmi content2presMatcher.cmi \
+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
+content2pres.cmi : termContentPres.cmi cicNotationPres.cmi
+renderingAttrs.cmo : renderingAttrs.cmi
+renderingAttrs.cmx : renderingAttrs.cmi
+cicNotationLexer.cmo : cicNotationLexer.cmi
+cicNotationLexer.cmx : cicNotationLexer.cmi
+cicNotationParser.cmo : cicNotationLexer.cmi cicNotationParser.cmi
+cicNotationParser.cmx : cicNotationLexer.cmx cicNotationParser.cmi
+mpresentation.cmo : mpresentation.cmi
+mpresentation.cmx : mpresentation.cmi
+box.cmo : renderingAttrs.cmi box.cmi
+box.cmx : renderingAttrs.cmx box.cmi
+content2presMatcher.cmo : content2presMatcher.cmi
+content2presMatcher.cmx : content2presMatcher.cmi
+termContentPres.cmo : renderingAttrs.cmi content2presMatcher.cmi \
     cicNotationParser.cmi termContentPres.cmi
-termContentPres.cmx: renderingAttrs.cmx content2presMatcher.cmx \
+termContentPres.cmx : renderingAttrs.cmx content2presMatcher.cmx \
     cicNotationParser.cmx termContentPres.cmi
-boxPp.cmo: renderingAttrs.cmi mpresentation.cmi cicNotationPres.cmi box.cmi \
+boxPp.cmo : renderingAttrs.cmi mpresentation.cmi cicNotationPres.cmi box.cmi \
     boxPp.cmi
-boxPp.cmx: renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx box.cmx \
+boxPp.cmx : renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx box.cmx \
     boxPp.cmi
-cicNotationPres.cmo: renderingAttrs.cmi mpresentation.cmi box.cmi \
+cicNotationPres.cmo : renderingAttrs.cmi mpresentation.cmi box.cmi \
     cicNotationPres.cmi
-cicNotationPres.cmx: renderingAttrs.cmx mpresentation.cmx box.cmx \
+cicNotationPres.cmx : renderingAttrs.cmx mpresentation.cmx box.cmx \
     cicNotationPres.cmi
-content2pres.cmo: termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \
+content2pres.cmo : termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \
     cicNotationPres.cmi box.cmi content2pres.cmi
-content2pres.cmx: termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \
+content2pres.cmx : termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \
     cicNotationPres.cmx box.cmx content2pres.cmi

diff --git a/matita/components/disambiguation/.depend b/matita/components/disambiguation/.depend
index fa6388aa7985f952fcfc356d09d10e7b467b7812..735bea7f72c4ccf1beef11818a346a3d4c3d6e6a 100644 (file)
--- a/matita/components/disambiguation/.depend
+++ b/matita/components/disambiguation/.depend
@@ -1,11 +1,11 @@
-disambiguateTypes.cmi:
-disambiguate.cmi: disambiguateTypes.cmi
-multiPassDisambiguator.cmi: disambiguateTypes.cmi disambiguate.cmi
-disambiguateTypes.cmo: disambiguateTypes.cmi
-disambiguateTypes.cmx: disambiguateTypes.cmi
-disambiguate.cmo: disambiguateTypes.cmi disambiguate.cmi
-disambiguate.cmx: disambiguateTypes.cmx disambiguate.cmi
-multiPassDisambiguator.cmo: disambiguateTypes.cmi disambiguate.cmi \
+disambiguateTypes.cmi :
+disambiguate.cmi : disambiguateTypes.cmi
+multiPassDisambiguator.cmi : disambiguateTypes.cmi disambiguate.cmi
+disambiguateTypes.cmo : disambiguateTypes.cmi
+disambiguateTypes.cmx : disambiguateTypes.cmi
+disambiguate.cmo : disambiguateTypes.cmi disambiguate.cmi
+disambiguate.cmx : disambiguateTypes.cmx disambiguate.cmi
+multiPassDisambiguator.cmo : disambiguateTypes.cmi disambiguate.cmi \
     multiPassDisambiguator.cmi
-multiPassDisambiguator.cmx: disambiguateTypes.cmx disambiguate.cmx \
+multiPassDisambiguator.cmx : disambiguateTypes.cmx disambiguate.cmx \
     multiPassDisambiguator.cmi

diff --git a/matita/components/extlib/.depend b/matita/components/extlib/.depend
index b121fbcd1d810f4f0921c4580bf8700bf63fc66a..e7b0a3bc74142a75bb82718931527b2b33db82e2 100644 (file)
--- a/matita/components/extlib/.depend
+++ b/matita/components/extlib/.depend
@@ -1,27 +1,27 @@
-componentsConf.cmi:
-hExtlib.cmi:
-hMarshal.cmi:
-patternMatcher.cmi:
-hLog.cmi:
-trie.cmi:
-discrimination_tree.cmi:
-hTopoSort.cmi:
-graphvizPp.cmi:
-componentsConf.cmo: componentsConf.cmi
-componentsConf.cmx: componentsConf.cmi
-hExtlib.cmo: hExtlib.cmi
-hExtlib.cmx: hExtlib.cmi
-hMarshal.cmo: hExtlib.cmi hMarshal.cmi
-hMarshal.cmx: hExtlib.cmx hMarshal.cmi
-patternMatcher.cmo: patternMatcher.cmi
-patternMatcher.cmx: patternMatcher.cmi
-hLog.cmo: hLog.cmi
-hLog.cmx: hLog.cmi
-trie.cmo: trie.cmi
-trie.cmx: trie.cmi
-discrimination_tree.cmo: trie.cmi hExtlib.cmi discrimination_tree.cmi
-discrimination_tree.cmx: trie.cmx hExtlib.cmx discrimination_tree.cmi
-hTopoSort.cmo: hTopoSort.cmi
-hTopoSort.cmx: hTopoSort.cmi
-graphvizPp.cmo: graphvizPp.cmi
-graphvizPp.cmx: graphvizPp.cmi
+componentsConf.cmi :
+hExtlib.cmi :
+hMarshal.cmi :
+patternMatcher.cmi :
+hLog.cmi :
+trie.cmi :
+discrimination_tree.cmi :
+hTopoSort.cmi :
+graphvizPp.cmi :
+componentsConf.cmo : componentsConf.cmi
+componentsConf.cmx : componentsConf.cmi
+hExtlib.cmo : hExtlib.cmi
+hExtlib.cmx : hExtlib.cmi
+hMarshal.cmo : hExtlib.cmi hMarshal.cmi
+hMarshal.cmx : hExtlib.cmx hMarshal.cmi
+patternMatcher.cmo : patternMatcher.cmi
+patternMatcher.cmx : patternMatcher.cmi
+hLog.cmo : hLog.cmi
+hLog.cmx : hLog.cmi
+trie.cmo : trie.cmi
+trie.cmx : trie.cmi
+discrimination_tree.cmo : trie.cmi hExtlib.cmi discrimination_tree.cmi
+discrimination_tree.cmx : trie.cmx hExtlib.cmx discrimination_tree.cmi
+hTopoSort.cmo : hTopoSort.cmi
+hTopoSort.cmx : hTopoSort.cmi
+graphvizPp.cmo : graphvizPp.cmi
+graphvizPp.cmx : graphvizPp.cmi

diff --git a/matita/components/getter/.depend b/matita/components/getter/.depend
index 600dc01db12608616635b2f813a625ac8ee02917..59c0b896e216c8aa3f904c2b1a721c13b87b4d83 100644 (file)
--- a/matita/components/getter/.depend
+++ b/matita/components/getter/.depend
@@ -1,38 +1,38 @@
-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
-http_getter_logger.cmx: http_getter_logger.cmi
-http_getter_misc.cmo: http_getter_logger.cmi http_getter_misc.cmi
-http_getter_misc.cmx: http_getter_logger.cmx http_getter_misc.cmi
-http_getter_const.cmo: http_getter_const.cmi
-http_getter_const.cmx: http_getter_const.cmi
-http_getter_env.cmo: http_getter_types.cmo http_getter_misc.cmi \
+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
+http_getter_logger.cmx : http_getter_logger.cmi
+http_getter_misc.cmo : http_getter_logger.cmi http_getter_misc.cmi
+http_getter_misc.cmx : http_getter_logger.cmx http_getter_misc.cmi
+http_getter_const.cmo : http_getter_const.cmi
+http_getter_const.cmx : http_getter_const.cmi
+http_getter_env.cmo : http_getter_types.cmo http_getter_misc.cmi \
     http_getter_logger.cmi http_getter_const.cmi http_getter_env.cmi
-http_getter_env.cmx: http_getter_types.cmx http_getter_misc.cmx \
+http_getter_env.cmx : http_getter_types.cmx http_getter_misc.cmx \
     http_getter_logger.cmx http_getter_const.cmx http_getter_env.cmi
-http_getter_storage.cmo: http_getter_wget.cmi http_getter_types.cmo \
+http_getter_storage.cmo : http_getter_wget.cmi http_getter_types.cmo \
     http_getter_misc.cmi http_getter_env.cmi http_getter_storage.cmi
-http_getter_storage.cmx: http_getter_wget.cmx http_getter_types.cmx \
+http_getter_storage.cmx : http_getter_wget.cmx http_getter_types.cmx \
     http_getter_misc.cmx http_getter_env.cmx http_getter_storage.cmi
-http_getter_common.cmo: http_getter_types.cmo http_getter_misc.cmi \
+http_getter_common.cmo : http_getter_types.cmo http_getter_misc.cmi \
     http_getter_logger.cmi http_getter_env.cmi http_getter_common.cmi
-http_getter_common.cmx: http_getter_types.cmx http_getter_misc.cmx \
+http_getter_common.cmx : http_getter_types.cmx http_getter_misc.cmx \
     http_getter_logger.cmx http_getter_env.cmx http_getter_common.cmi
-http_getter.cmo: http_getter_wget.cmi http_getter_types.cmo \
+http_getter.cmo : http_getter_wget.cmi http_getter_types.cmo \
     http_getter_storage.cmi http_getter_misc.cmi http_getter_logger.cmi \
     http_getter_env.cmi http_getter_const.cmi http_getter_common.cmi \
     http_getter.cmi
-http_getter.cmx: http_getter_wget.cmx http_getter_types.cmx \
+http_getter.cmx : http_getter_wget.cmx http_getter_types.cmx \
     http_getter_storage.cmx http_getter_misc.cmx http_getter_logger.cmx \
     http_getter_env.cmx http_getter_const.cmx http_getter_common.cmx \
     http_getter.cmi

diff --git a/matita/components/grafite/.depend b/matita/components/grafite/.depend
index ba4fab03aa74e53b224fc1e4e5db4b8d24e2073b..e70c83c775c2c4c31f9f428867d0ef7b521ef616 100644 (file)
--- a/matita/components/grafite/.depend
+++ b/matita/components/grafite/.depend
@@ -1,5 +1,5 @@
-grafiteAstPp.cmi: grafiteAst.cmo
-grafiteAst.cmo:
-grafiteAst.cmx:
-grafiteAstPp.cmo: grafiteAst.cmo grafiteAstPp.cmi
-grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi
+grafiteAstPp.cmi : grafiteAst.cmo
+grafiteAst.cmo :
+grafiteAst.cmx :
+grafiteAstPp.cmo : grafiteAst.cmo grafiteAstPp.cmi
+grafiteAstPp.cmx : grafiteAst.cmx grafiteAstPp.cmi

diff --git a/matita/components/grafite_engine/.depend b/matita/components/grafite_engine/.depend
index 27787b008a0fd68ab2fe0e21a32de1e5bc0d977e..e6d4942c67b319e5e52866b737ef24ee4091860e 100644 (file)
--- a/matita/components/grafite_engine/.depend
+++ b/matita/components/grafite_engine/.depend
@@ -1,11 +1,11 @@
-grafiteTypes.cmi:
-nCicCoercDeclaration.cmi: grafiteTypes.cmi
-grafiteEngine.cmi: grafiteTypes.cmi
-grafiteTypes.cmo: grafiteTypes.cmi
-grafiteTypes.cmx: grafiteTypes.cmi
-nCicCoercDeclaration.cmo: grafiteTypes.cmi nCicCoercDeclaration.cmi
-nCicCoercDeclaration.cmx: grafiteTypes.cmx nCicCoercDeclaration.cmi
-grafiteEngine.cmo: nCicCoercDeclaration.cmi grafiteTypes.cmi \
+grafiteTypes.cmi :
+nCicCoercDeclaration.cmi : grafiteTypes.cmi
+grafiteEngine.cmi : grafiteTypes.cmi
+grafiteTypes.cmo : grafiteTypes.cmi
+grafiteTypes.cmx : grafiteTypes.cmi
+nCicCoercDeclaration.cmo : grafiteTypes.cmi nCicCoercDeclaration.cmi
+nCicCoercDeclaration.cmx : grafiteTypes.cmx nCicCoercDeclaration.cmi
+grafiteEngine.cmo : nCicCoercDeclaration.cmi grafiteTypes.cmi \
     grafiteEngine.cmi
-grafiteEngine.cmx: nCicCoercDeclaration.cmx grafiteTypes.cmx \
+grafiteEngine.cmx : nCicCoercDeclaration.cmx grafiteTypes.cmx \
     grafiteEngine.cmi

diff --git a/matita/components/grafite_parser/.depend b/matita/components/grafite_parser/.depend
index 5142da1bf4ce3d4744fd0df8c6ea3070f545436c..752b0d88d5ca9ccf9f59da28b6578d37e2a58763 100644 (file)
--- a/matita/components/grafite_parser/.depend
+++ b/matita/components/grafite_parser/.depend
@@ -1,6 +1,6 @@
-grafiteParser.cmi:
-print_grammar.cmi: grafiteParser.cmi
-grafiteParser.cmo: grafiteParser.cmi
-grafiteParser.cmx: grafiteParser.cmi
-print_grammar.cmo: print_grammar.cmi
-print_grammar.cmx: print_grammar.cmi
+grafiteParser.cmi :
+print_grammar.cmi : grafiteParser.cmi
+grafiteParser.cmo : grafiteParser.cmi
+grafiteParser.cmx : grafiteParser.cmi
+print_grammar.cmo : print_grammar.cmi
+print_grammar.cmx : print_grammar.cmi

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index 112970d3e38f5f3aeb4219bc78752f390cd298cc..70fe2f4157621800d93c37c44f4442182d675d54 100644 (file)
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -58,12 +58,12 @@ let add_raw_attribute ~text t = N.AttributedTerm (`Raw text, t)
 
 let default_associativity = Gramext.NonA
         
-let mk_rec_corec ind_kind defs loc = 
- let attrs = `Provided, `Definition, `Regular in
+let mk_rec_corec src ind_kind defs loc = 
+ let attrs = src, `Definition, `Regular in
   (loc, N.LetRec (ind_kind, defs, attrs))
 
-let nmk_rec_corec ind_kind defs loc index = 
- let loc,t = mk_rec_corec ind_kind defs loc in
+let nmk_rec_corec src ind_kind defs loc index = 
+ let loc,t = mk_rec_corec src ind_kind defs loc in
   G.NObj (loc,t,index)
 
 (*
@@ -493,34 +493,41 @@ EXTEND
 
   index: [[ b = OPT SYMBOL "-" -> match b with None -> true | _ -> false ]];
 
+  source: [[
+     src = OPT IDENT "implied" ->
+        match src with None -> `Provided | _ -> `Implied
+  ]];
+
   grafite_ncommand: [ [
       IDENT "qed" ;  i = index -> G.NQed (loc,i)
     | IDENT "defined" ;  i = index -> G.NQed (loc,i) (* FG: presentational qed for definitions *)
-    | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
+    | src = source; nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
-        let attrs = `Provided, nflavour, `Regular in
+        let attrs = src, nflavour, `Regular in
        G.NObj (loc, N.Theorem (name, typ, body, attrs),true)
-    | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
+    | src = source; nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
       body = term ->
-        let attrs = `Provided, nflavour, `Regular in
+        let attrs = src, nflavour, `Regular in
         G.NObj (loc, 
           N.Theorem(name, N.Implicit `JustOne, Some body, attrs),
           true)
-    | IDENT "axiom"; i = index; name = IDENT; SYMBOL ":"; typ = term ->
-        let attrs = `Provided, `Axiom, `Regular in
+    | src = source; IDENT "axiom"; i = index; name = IDENT; SYMBOL ":"; typ = term ->
+        let attrs = src, `Axiom, `Regular in
        G.NObj (loc, N.Theorem (name, typ, None, attrs),i)
     | IDENT "discriminator" ; indty = tactic_term -> G.NDiscriminator (loc,indty)
     | IDENT "inverter"; name = IDENT; IDENT "for" ; indty = tactic_term ;
       paramspec = OPT inverter_param_list ; 
       outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] -> 
         G.NInverter (loc,name,indty,paramspec,outsort)
-    | LETCOREC ; defs = let_codefs -> 
-        nmk_rec_corec `CoInductive defs loc true
-    | LETREC ; defs = let_defs -> 
-        nmk_rec_corec `Inductive defs loc true
+    | src = source; LETCOREC ; defs = let_codefs -> 
+        nmk_rec_corec src `CoInductive defs loc true
+    | src = source; LETREC ; defs = let_defs -> 
+        nmk_rec_corec src `Inductive defs loc true
+(* FG: no source since no i_attr in N.Inductive *)
     | IDENT "inductive"; spec = inductive_spec ->
         let (params, ind_types) = spec in
         G.NObj (loc, N.Inductive (params, ind_types),true)
+(* FG: no source since no i_attr in N.Inductive *)
     | IDENT "coinductive"; spec = inductive_spec ->
         let (params, ind_types) = spec in
         let ind_types = (* set inductive flags to false (coinductive) *)
@@ -548,6 +555,7 @@ EXTEND
         "to"; target = term -> t,ty,(id,source),target ] ->
           let compose = compose = None in
           G.NCoercion(loc,name,compose,spec)
+(* FG: no source since no i_attr in N.Record *)
     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
         G.NObj (loc, N.Record (params,name,ty,fields),true)
     | IDENT "copy" ; s = IDENT; IDENT "from"; u = URI; "with"; 

diff --git a/matita/components/library/.depend b/matita/components/library/.depend
index 28703386aad00a4e2a16e2783eefcc8461815e3e..6f2769b943d3b17c0eaa88d03ff693cda70b64e2 100644 (file)
--- a/matita/components/library/.depend
+++ b/matita/components/library/.depend
@@ -1,9 +1,9 @@
-librarian.cmi:
-libraryMisc.cmi:
-libraryClean.cmi:
-librarian.cmo: librarian.cmi
-librarian.cmx: librarian.cmi
-libraryMisc.cmo: libraryMisc.cmi
-libraryMisc.cmx: libraryMisc.cmi
-libraryClean.cmo: libraryClean.cmi
-libraryClean.cmx: libraryClean.cmi
+librarian.cmi :
+libraryMisc.cmi :
+libraryClean.cmi :
+librarian.cmo : librarian.cmi
+librarian.cmx : librarian.cmi
+libraryMisc.cmo : libraryMisc.cmi
+libraryMisc.cmx : libraryMisc.cmi
+libraryClean.cmo : libraryClean.cmi
+libraryClean.cmx : libraryClean.cmi

diff --git a/matita/components/logger/.depend b/matita/components/logger/.depend
index 1c8ec5b7c84887d66524df89f46cd7730c64fcc4..d1b4c37162663daab85eee7845f39b2422456992 100644 (file)
--- a/matita/components/logger/.depend
+++ b/matita/components/logger/.depend
@@ -1,3 +1,3 @@
-helmLogger.cmi:
-helmLogger.cmo: helmLogger.cmi
-helmLogger.cmx: helmLogger.cmi
+helmLogger.cmi :
+helmLogger.cmo : helmLogger.cmi
+helmLogger.cmx : helmLogger.cmi

diff --git a/matita/components/ng_cic_content/.depend b/matita/components/ng_cic_content/.depend
index b1a499fd3facc2d07103b73c013e3750d0b151da..01e2f5b1ef6d52b1677f749f6a30ec2eb6ed65db 100644 (file)
--- a/matita/components/ng_cic_content/.depend
+++ b/matita/components/ng_cic_content/.depend
@@ -1,6 +1,6 @@
-ncic2astMatcher.cmi:
-interpretations.cmi:
-ncic2astMatcher.cmo: ncic2astMatcher.cmi
-ncic2astMatcher.cmx: ncic2astMatcher.cmi
-interpretations.cmo: ncic2astMatcher.cmi interpretations.cmi
-interpretations.cmx: ncic2astMatcher.cmx interpretations.cmi
+ncic2astMatcher.cmi :
+interpretations.cmi :
+ncic2astMatcher.cmo : ncic2astMatcher.cmi
+ncic2astMatcher.cmx : ncic2astMatcher.cmi
+interpretations.cmo : ncic2astMatcher.cmi interpretations.cmi
+interpretations.cmx : ncic2astMatcher.cmx interpretations.cmi

diff --git a/matita/components/ng_disambiguation/.depend b/matita/components/ng_disambiguation/.depend
index d5306074ab892a33a75040bd24e990df97bc7357..79fd839b24f42bc72c2f7a9221dfa9fc047acb37 100644 (file)
--- a/matita/components/ng_disambiguation/.depend
+++ b/matita/components/ng_disambiguation/.depend
@@ -1,14 +1,14 @@
-nnumber_notation.cmi:
-disambiguateChoices.cmi:
-nCicDisambiguate.cmi:
-grafiteDisambiguate.cmi:
-nnumber_notation.cmo: nnumber_notation.cmi
-nnumber_notation.cmx: nnumber_notation.cmi
-disambiguateChoices.cmo: nnumber_notation.cmi disambiguateChoices.cmi
-disambiguateChoices.cmx: nnumber_notation.cmx disambiguateChoices.cmi
-nCicDisambiguate.cmo: nCicDisambiguate.cmi
-nCicDisambiguate.cmx: nCicDisambiguate.cmi
-grafiteDisambiguate.cmo: nCicDisambiguate.cmi disambiguateChoices.cmi \
+nnumber_notation.cmi :
+disambiguateChoices.cmi :
+nCicDisambiguate.cmi :
+grafiteDisambiguate.cmi :
+nnumber_notation.cmo : nnumber_notation.cmi
+nnumber_notation.cmx : nnumber_notation.cmi
+disambiguateChoices.cmo : nnumber_notation.cmi disambiguateChoices.cmi
+disambiguateChoices.cmx : nnumber_notation.cmx disambiguateChoices.cmi
+nCicDisambiguate.cmo : nCicDisambiguate.cmi
+nCicDisambiguate.cmx : nCicDisambiguate.cmi
+grafiteDisambiguate.cmo : nCicDisambiguate.cmi disambiguateChoices.cmi \
     grafiteDisambiguate.cmi
-grafiteDisambiguate.cmx: nCicDisambiguate.cmx disambiguateChoices.cmx \
+grafiteDisambiguate.cmx : nCicDisambiguate.cmx disambiguateChoices.cmx \
     grafiteDisambiguate.cmi

diff --git a/matita/components/ng_extraction/.depend b/matita/components/ng_extraction/.depend
new file mode 100644 (file)
index 0000000..c2ad6ff
--- /dev/null
+++ b/matita/components/ng_extraction/.depend
@@ -0,0 +1,34 @@
+nCicExtraction.cmi :
+coq.cmi :
+ocamlExtractionTable.cmi : miniml.cmo coq.cmi
+mlutil.cmi : ocamlExtractionTable.cmi miniml.cmo coq.cmi
+common.cmi : ocamlExtractionTable.cmi mlutil.cmi miniml.cmo coq.cmi
+extraction.cmi : ocamlExtractionTable.cmi miniml.cmo coq.cmi
+ocaml.cmi : ocamlExtractionTable.cmi miniml.cmo coq.cmi
+ocamlExtraction.cmi : ocamlExtractionTable.cmi
+miniml.cmo : coq.cmi
+miniml.cmx : coq.cmx
+nCicExtraction.cmo : nCicExtraction.cmi
+nCicExtraction.cmx : nCicExtraction.cmi
+coq.cmo : coq.cmi
+coq.cmx : coq.cmi
+ocamlExtractionTable.cmo : miniml.cmo coq.cmi ocamlExtractionTable.cmi
+ocamlExtractionTable.cmx : miniml.cmx coq.cmx ocamlExtractionTable.cmi
+mlutil.cmo : ocamlExtractionTable.cmi miniml.cmo coq.cmi mlutil.cmi
+mlutil.cmx : ocamlExtractionTable.cmx miniml.cmx coq.cmx mlutil.cmi
+common.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmo coq.cmi \
+    common.cmi
+common.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \
+    common.cmi
+extraction.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmo coq.cmi \
+    common.cmi extraction.cmi
+extraction.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \
+    common.cmx extraction.cmi
+ocaml.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmo coq.cmi \
+    common.cmi ocaml.cmi
+ocaml.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \
+    common.cmx ocaml.cmi
+ocamlExtraction.cmo : ocamlExtractionTable.cmi ocaml.cmi extraction.cmi \
+    coq.cmi ocamlExtraction.cmi
+ocamlExtraction.cmx : ocamlExtractionTable.cmx ocaml.cmx extraction.cmx \
+    coq.cmx ocamlExtraction.cmi

diff --git a/matita/components/ng_kernel/.depend b/matita/components/ng_kernel/.depend
index 16f0d02cce32e0673a5ebae845e6a94b88f9d1a2..a55f8728476514e27fc165bf6c7931bc34089f59 100644 (file)
--- a/matita/components/ng_kernel/.depend
+++ b/matita/components/ng_kernel/.depend
@@ -1,41 +1,41 @@
-nUri.cmi:
-nReference.cmi: nUri.cmi
-nCicUtils.cmi: nCic.cmo
-nCicSubstitution.cmi: nCic.cmo
-nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmo
-nCicReduction.cmi: nCic.cmo
-nCicTypeChecker.cmi: nUri.cmi nReference.cmi nCic.cmo
-nCicUntrusted.cmi: nCic.cmo
-nCicPp.cmi: nReference.cmi nCic.cmo
-nCic.cmo: nUri.cmi nReference.cmi
-nCic.cmx: nUri.cmx nReference.cmx
-nUri.cmo: nUri.cmi
-nUri.cmx: nUri.cmi
-nReference.cmo: nUri.cmi nReference.cmi
-nReference.cmx: nUri.cmx nReference.cmi
-nCicUtils.cmo: nReference.cmi nCic.cmo nCicUtils.cmi
-nCicUtils.cmx: nReference.cmx nCic.cmx nCicUtils.cmi
-nCicSubstitution.cmo: nReference.cmi nCicUtils.cmi nCic.cmo \
+nUri.cmi :
+nReference.cmi : nUri.cmi
+nCicUtils.cmi : nCic.cmo
+nCicSubstitution.cmi : nCic.cmo
+nCicEnvironment.cmi : nUri.cmi nReference.cmi nCic.cmo
+nCicReduction.cmi : nCic.cmo
+nCicTypeChecker.cmi : nUri.cmi nReference.cmi nCic.cmo
+nCicUntrusted.cmi : nCic.cmo
+nCicPp.cmi : nReference.cmi nCic.cmo
+nCic.cmo : nUri.cmi nReference.cmi
+nCic.cmx : nUri.cmx nReference.cmx
+nUri.cmo : nUri.cmi
+nUri.cmx : nUri.cmi
+nReference.cmo : nUri.cmi nReference.cmi
+nReference.cmx : nUri.cmx nReference.cmi
+nCicUtils.cmo : nReference.cmi nCic.cmo nCicUtils.cmi
+nCicUtils.cmx : nReference.cmx nCic.cmx nCicUtils.cmi
+nCicSubstitution.cmo : nReference.cmi nCicUtils.cmi nCic.cmo \
     nCicSubstitution.cmi
-nCicSubstitution.cmx: nReference.cmx nCicUtils.cmx nCic.cmx \
+nCicSubstitution.cmx : nReference.cmx nCicUtils.cmx nCic.cmx \
     nCicSubstitution.cmi
-nCicEnvironment.cmo: nUri.cmi nReference.cmi nCic.cmo nCicEnvironment.cmi
-nCicEnvironment.cmx: nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi
-nCicReduction.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \
+nCicEnvironment.cmo : nUri.cmi nReference.cmi nCic.cmo nCicEnvironment.cmi
+nCicEnvironment.cmx : nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi
+nCicReduction.cmo : nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \
     nCicEnvironment.cmi nCic.cmo nCicReduction.cmi
-nCicReduction.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \
+nCicReduction.cmx : nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \
     nCicEnvironment.cmx nCic.cmx nCicReduction.cmi
-nCicTypeChecker.cmo: nUri.cmi nReference.cmi nCicUtils.cmi \
+nCicTypeChecker.cmo : nUri.cmi nReference.cmi nCicUtils.cmi \
     nCicSubstitution.cmi nCicReduction.cmi nCicEnvironment.cmi nCic.cmo \
     nCicTypeChecker.cmi
-nCicTypeChecker.cmx: nUri.cmx nReference.cmx nCicUtils.cmx \
+nCicTypeChecker.cmx : nUri.cmx nReference.cmx nCicUtils.cmx \
     nCicSubstitution.cmx nCicReduction.cmx nCicEnvironment.cmx nCic.cmx \
     nCicTypeChecker.cmi
-nCicUntrusted.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \
+nCicUntrusted.cmo : nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \
     nCicReduction.cmi nCicEnvironment.cmi nCic.cmo nCicUntrusted.cmi
-nCicUntrusted.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \
+nCicUntrusted.cmx : nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \
     nCicReduction.cmx nCicEnvironment.cmx nCic.cmx nCicUntrusted.cmi
-nCicPp.cmo: nUri.cmi nReference.cmi nCicSubstitution.cmi nCicReduction.cmi \
+nCicPp.cmo : nUri.cmi nReference.cmi nCicSubstitution.cmi nCicReduction.cmi \
     nCicEnvironment.cmi nCic.cmo nCicPp.cmi
-nCicPp.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \
+nCicPp.cmx : nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \
     nCicEnvironment.cmx nCic.cmx nCicPp.cmi

diff --git a/matita/components/ng_kernel/nCic.ml b/matita/components/ng_kernel/nCic.ml
index 94dc827c810df412dc5d3c4a5a545885bc5a8058..03672a0c46c2d9c446fb4a6b5075b6c226b239d0 100644 (file)
--- a/matita/components/ng_kernel/nCic.ml
+++ b/matita/components/ng_kernel/nCic.ml
@@ -104,11 +104,14 @@ type ind_pragma = (* pragmatic of the object *)
   (* inductive type that encodes a record; the arguments are the record 
    * fields names and if they are coercions and then the coercion arity *)
 
-type generated = [ `Generated | `Provided ]
-
-type c_attr = generated * def_flavour * def_pragma
-type f_attr = generated * def_flavour * def_pragma
-type i_attr = generated * ind_pragma
+type source = [ `Generated (* generated by matita *)
+              | `Provided  (* provided by the user directly or from another ITP *)
+              | `Implied   (* provided as generated by another ITP *)
+              ]
+
+type c_attr = source * def_flavour * def_pragma
+type f_attr = source * def_flavour * def_pragma
+type i_attr = source * ind_pragma
 
  (* invariant: metasenv and substitution have disjoint domains *)
 type obj_kind =

diff --git a/matita/components/ng_kernel/nCicPp.ml b/matita/components/ng_kernel/nCicPp.ml
index 11ba55e787c0a192dfe53e3773f0e36ecc75cd1b..5a99a0664e111c40d2ca8de893d54185051ccb8d 100644 (file)
--- a/matita/components/ng_kernel/nCicPp.ml
+++ b/matita/components/ng_kernel/nCicPp.ml
@@ -263,6 +263,7 @@ let ppsubst status ~formatter ~metasenv ?(use_subst=true) subst =
 let string_of_generated = function
   | `Generated -> "Generated"
   | `Provided -> "Provided"
+  | `Implied -> "Implied"
 ;;
 
 let string_of_flavour = function

diff --git a/matita/components/ng_library/.depend b/matita/components/ng_library/.depend
index b9e7731f94c582d4210a0185df5e6ad92294f343..a571a865c12712184f2df7cb39b8afb4191c4cf5 100644 (file)
--- a/matita/components/ng_library/.depend
+++ b/matita/components/ng_library/.depend
@@ -1,3 +1,3 @@
-nCicLibrary.cmi:
-nCicLibrary.cmo: nCicLibrary.cmi
-nCicLibrary.cmx: nCicLibrary.cmi
+nCicLibrary.cmi :
+nCicLibrary.cmo : nCicLibrary.cmi
+nCicLibrary.cmx : nCicLibrary.cmi

diff --git a/matita/components/ng_paramodulation/.depend b/matita/components/ng_paramodulation/.depend
index 4e9e21a19dea6dad44753808a4f7d6af97339701..5f4f1cc562e40087cacaebc42ee367dc784ebae6 100644 (file)
--- a/matita/components/ng_paramodulation/.depend
+++ b/matita/components/ng_paramodulation/.depend
@@ -1,45 +1,45 @@
-terms.cmi:
-pp.cmi: terms.cmi
-foSubst.cmi: terms.cmi
-orderings.cmi: terms.cmi
-foUtils.cmi: terms.cmi orderings.cmi
-foUnif.cmi: terms.cmi orderings.cmi
-index.cmi: terms.cmi orderings.cmi
-superposition.cmi: terms.cmi orderings.cmi index.cmi
-stats.cmi: terms.cmi orderings.cmi
-paramod.cmi: terms.cmi orderings.cmi
-nCicBlob.cmi: terms.cmi
-nCicProof.cmi: terms.cmi
-nCicParamod.cmi: terms.cmi
-terms.cmo: terms.cmi
-terms.cmx: terms.cmi
-pp.cmo: terms.cmi pp.cmi
-pp.cmx: terms.cmx pp.cmi
-foSubst.cmo: terms.cmi foSubst.cmi
-foSubst.cmx: terms.cmx foSubst.cmi
-orderings.cmo: terms.cmi pp.cmi foSubst.cmi orderings.cmi
-orderings.cmx: terms.cmx pp.cmx foSubst.cmx orderings.cmi
-foUtils.cmo: terms.cmi orderings.cmi foSubst.cmi foUtils.cmi
-foUtils.cmx: terms.cmx orderings.cmx foSubst.cmx foUtils.cmi
-foUnif.cmo: terms.cmi orderings.cmi foUtils.cmi foSubst.cmi foUnif.cmi
-foUnif.cmx: terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi
-index.cmo: terms.cmi pp.cmi orderings.cmi foUtils.cmi foUnif.cmi index.cmi
-index.cmx: terms.cmx pp.cmx orderings.cmx foUtils.cmx foUnif.cmx index.cmi
-superposition.cmo: terms.cmi pp.cmi orderings.cmi index.cmi foUtils.cmi \
+terms.cmi :
+pp.cmi : terms.cmi
+foSubst.cmi : terms.cmi
+orderings.cmi : terms.cmi
+foUtils.cmi : terms.cmi orderings.cmi
+foUnif.cmi : terms.cmi orderings.cmi
+index.cmi : terms.cmi orderings.cmi
+superposition.cmi : terms.cmi orderings.cmi index.cmi
+stats.cmi : terms.cmi orderings.cmi
+paramod.cmi : terms.cmi orderings.cmi
+nCicBlob.cmi : terms.cmi
+nCicProof.cmi : terms.cmi
+nCicParamod.cmi : terms.cmi
+terms.cmo : terms.cmi
+terms.cmx : terms.cmi
+pp.cmo : terms.cmi pp.cmi
+pp.cmx : terms.cmx pp.cmi
+foSubst.cmo : terms.cmi foSubst.cmi
+foSubst.cmx : terms.cmx foSubst.cmi
+orderings.cmo : terms.cmi pp.cmi foSubst.cmi orderings.cmi
+orderings.cmx : terms.cmx pp.cmx foSubst.cmx orderings.cmi
+foUtils.cmo : terms.cmi orderings.cmi foSubst.cmi foUtils.cmi
+foUtils.cmx : terms.cmx orderings.cmx foSubst.cmx foUtils.cmi
+foUnif.cmo : terms.cmi orderings.cmi foUtils.cmi foSubst.cmi foUnif.cmi
+foUnif.cmx : terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi
+index.cmo : terms.cmi pp.cmi orderings.cmi foUtils.cmi foUnif.cmi index.cmi
+index.cmx : terms.cmx pp.cmx orderings.cmx foUtils.cmx foUnif.cmx index.cmi
+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 \
+superposition.cmx : terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \
     foUnif.cmx foSubst.cmx superposition.cmi
-stats.cmo: terms.cmi stats.cmi
-stats.cmx: terms.cmx stats.cmi
-paramod.cmo: terms.cmi superposition.cmi pp.cmi orderings.cmi index.cmi \
+stats.cmo : terms.cmi stats.cmi
+stats.cmx : terms.cmx stats.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 \
+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
-nCicProof.cmo: terms.cmi pp.cmi nCicBlob.cmi foSubst.cmi nCicProof.cmi
-nCicProof.cmx: terms.cmx pp.cmx nCicBlob.cmx foSubst.cmx nCicProof.cmi
-nCicParamod.cmo: terms.cmi pp.cmi paramod.cmi orderings.cmi nCicProof.cmi \
+nCicBlob.cmo : terms.cmi foUtils.cmi nCicBlob.cmi
+nCicBlob.cmx : terms.cmx foUtils.cmx nCicBlob.cmi
+nCicProof.cmo : terms.cmi pp.cmi nCicBlob.cmi foSubst.cmi nCicProof.cmi
+nCicProof.cmx : terms.cmx pp.cmx nCicBlob.cmx foSubst.cmx nCicProof.cmi
+nCicParamod.cmo : terms.cmi pp.cmi paramod.cmi orderings.cmi nCicProof.cmi \
     nCicBlob.cmi nCicParamod.cmi
-nCicParamod.cmx: terms.cmx pp.cmx paramod.cmx orderings.cmx nCicProof.cmx \
+nCicParamod.cmx : terms.cmx pp.cmx paramod.cmx orderings.cmx nCicProof.cmx \
     nCicBlob.cmx nCicParamod.cmi

diff --git a/matita/components/ng_refiner/.depend b/matita/components/ng_refiner/.depend
index 5e055ecdc7551278526253a111a618f70f91f278..d8295760aff118a07e4066718ff8146fb64f0228 100644 (file)
--- a/matita/components/ng_refiner/.depend
+++ b/matita/components/ng_refiner/.depend
@@ -1,25 +1,27 @@
-nDiscriminationTree.cmi:
-nCicMetaSubst.cmi:
-nCicUnifHint.cmi:
-nCicCoercion.cmi: nCicUnifHint.cmi
-nCicRefineUtil.cmi:
-nCicUnification.cmi: nCicCoercion.cmi
-nCicRefiner.cmi: nCicCoercion.cmi
-nDiscriminationTree.cmo: nDiscriminationTree.cmi
-nDiscriminationTree.cmx: nDiscriminationTree.cmi
-nCicMetaSubst.cmo: nCicMetaSubst.cmi
-nCicMetaSubst.cmx: nCicMetaSubst.cmi
-nCicUnifHint.cmo: nDiscriminationTree.cmi nCicMetaSubst.cmi nCicUnifHint.cmi
-nCicUnifHint.cmx: nDiscriminationTree.cmx nCicMetaSubst.cmx nCicUnifHint.cmi
-nCicCoercion.cmo: nDiscriminationTree.cmi nCicUnifHint.cmi nCicMetaSubst.cmi \
-    nCicCoercion.cmi
-nCicCoercion.cmx: nDiscriminationTree.cmx nCicUnifHint.cmx nCicMetaSubst.cmx \
-    nCicCoercion.cmi
-nCicRefineUtil.cmo: nCicMetaSubst.cmi nCicRefineUtil.cmi
-nCicRefineUtil.cmx: nCicMetaSubst.cmx nCicRefineUtil.cmi
-nCicUnification.cmo: nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi
-nCicUnification.cmx: nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi
-nCicRefiner.cmo: nCicUnification.cmi nCicRefineUtil.cmi nCicMetaSubst.cmi \
+nDiscriminationTree.cmi :
+nCicMetaSubst.cmi :
+nCicUnifHint.cmi :
+nCicCoercion.cmi : nCicUnifHint.cmi
+nCicRefineUtil.cmi :
+nCicUnification.cmi : nCicCoercion.cmi
+nCicRefiner.cmi : nCicCoercion.cmi
+nDiscriminationTree.cmo : nDiscriminationTree.cmi
+nDiscriminationTree.cmx : nDiscriminationTree.cmi
+nCicMetaSubst.cmo : nCicMetaSubst.cmi
+nCicMetaSubst.cmx : nCicMetaSubst.cmi
+nCicUnifHint.cmo : nDiscriminationTree.cmi nCicMetaSubst.cmi \
+    nCicUnifHint.cmi
+nCicUnifHint.cmx : nDiscriminationTree.cmx nCicMetaSubst.cmx \
+    nCicUnifHint.cmi
+nCicCoercion.cmo : nDiscriminationTree.cmi nCicUnifHint.cmi \
+    nCicMetaSubst.cmi nCicCoercion.cmi
+nCicCoercion.cmx : nDiscriminationTree.cmx nCicUnifHint.cmx \
+    nCicMetaSubst.cmx nCicCoercion.cmi
+nCicRefineUtil.cmo : nCicMetaSubst.cmi nCicRefineUtil.cmi
+nCicRefineUtil.cmx : nCicMetaSubst.cmx nCicRefineUtil.cmi
+nCicUnification.cmo : nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi
+nCicUnification.cmx : nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi
+nCicRefiner.cmo : nCicUnification.cmi nCicRefineUtil.cmi nCicMetaSubst.cmi \
     nCicCoercion.cmi nCicRefiner.cmi
-nCicRefiner.cmx: nCicUnification.cmx nCicRefineUtil.cmx nCicMetaSubst.cmx \
+nCicRefiner.cmx : nCicUnification.cmx nCicRefineUtil.cmx nCicMetaSubst.cmx \
     nCicCoercion.cmx nCicRefiner.cmi

diff --git a/matita/components/ng_tactics/.depend b/matita/components/ng_tactics/.depend
index 3e01ca0fba9904f473324a20e3c1db89ce99fc63..e8ca8210ee825eaece6fe84e2aea51b7174d36ad 100644 (file)
--- a/matita/components/ng_tactics/.depend
+++ b/matita/components/ng_tactics/.depend
@@ -1,30 +1,30 @@
-continuationals.cmi:
-nCicTacReduction.cmi:
-nTacStatus.cmi: continuationals.cmi
-nCicElim.cmi:
-nTactics.cmi: nTacStatus.cmi
-nnAuto.cmi: nTacStatus.cmi
-nDestructTac.cmi: nTacStatus.cmi
-nInversion.cmi: nTacStatus.cmi
-continuationals.cmo: continuationals.cmi
-continuationals.cmx: continuationals.cmi
-nCicTacReduction.cmo: nCicTacReduction.cmi
-nCicTacReduction.cmx: nCicTacReduction.cmi
-nTacStatus.cmo: nCicTacReduction.cmi continuationals.cmi nTacStatus.cmi
-nTacStatus.cmx: nCicTacReduction.cmx continuationals.cmx nTacStatus.cmi
-nCicElim.cmo: nCicElim.cmi
-nCicElim.cmx: nCicElim.cmi
-nTactics.cmo: nTacStatus.cmi nCicElim.cmi continuationals.cmi nTactics.cmi
-nTactics.cmx: nTacStatus.cmx nCicElim.cmx continuationals.cmx nTactics.cmi
-nnAuto.cmo: nTactics.cmi nTacStatus.cmi nCicTacReduction.cmi \
+continuationals.cmi :
+nCicTacReduction.cmi :
+nTacStatus.cmi : continuationals.cmi
+nCicElim.cmi :
+nTactics.cmi : nTacStatus.cmi
+nnAuto.cmi : nTacStatus.cmi
+nDestructTac.cmi : nTacStatus.cmi
+nInversion.cmi : nTacStatus.cmi
+continuationals.cmo : continuationals.cmi
+continuationals.cmx : continuationals.cmi
+nCicTacReduction.cmo : nCicTacReduction.cmi
+nCicTacReduction.cmx : nCicTacReduction.cmi
+nTacStatus.cmo : nCicTacReduction.cmi continuationals.cmi nTacStatus.cmi
+nTacStatus.cmx : nCicTacReduction.cmx continuationals.cmx nTacStatus.cmi
+nCicElim.cmo : nCicElim.cmi
+nCicElim.cmx : nCicElim.cmi
+nTactics.cmo : nTacStatus.cmi nCicElim.cmi continuationals.cmi nTactics.cmi
+nTactics.cmx : nTacStatus.cmx nCicElim.cmx continuationals.cmx nTactics.cmi
+nnAuto.cmo : nTactics.cmi nTacStatus.cmi nCicTacReduction.cmi \
     continuationals.cmi nnAuto.cmi
-nnAuto.cmx: nTactics.cmx nTacStatus.cmx nCicTacReduction.cmx \
+nnAuto.cmx : nTactics.cmx nTacStatus.cmx nCicTacReduction.cmx \
     continuationals.cmx nnAuto.cmi
-nDestructTac.cmo: nTactics.cmi nTacStatus.cmi continuationals.cmi \
+nDestructTac.cmo : nTactics.cmi nTacStatus.cmi continuationals.cmi \
     nDestructTac.cmi
-nDestructTac.cmx: nTactics.cmx nTacStatus.cmx continuationals.cmx \
+nDestructTac.cmx : nTactics.cmx nTacStatus.cmx continuationals.cmx \
     nDestructTac.cmi
-nInversion.cmo: nTactics.cmi nTacStatus.cmi nCicElim.cmi continuationals.cmi \
-    nInversion.cmi
-nInversion.cmx: nTactics.cmx nTacStatus.cmx nCicElim.cmx continuationals.cmx \
-    nInversion.cmi
+nInversion.cmo : nTactics.cmi nTacStatus.cmi nCicElim.cmi \
+    continuationals.cmi nInversion.cmi
+nInversion.cmx : nTactics.cmx nTacStatus.cmx nCicElim.cmx \
+    continuationals.cmx nInversion.cmi

diff --git a/matita/components/registry/.depend b/matita/components/registry/.depend
index 19a1fd3259d6d4ffaa737eaa6b604187e7540bd7..67113e67f7af0c0d4e8e6ae696d91d217f620df6 100644 (file)
--- a/matita/components/registry/.depend
+++ b/matita/components/registry/.depend
@@ -1,3 +1,3 @@
-helm_registry.cmi:
-helm_registry.cmo: helm_registry.cmi
-helm_registry.cmx: helm_registry.cmi
+helm_registry.cmi :
+helm_registry.cmo : helm_registry.cmi
+helm_registry.cmx : helm_registry.cmi

diff --git a/matita/components/thread/.depend b/matita/components/thread/.depend
index e25145b8b1499b6c59f701cc8a2e4269b3b0e56b..d68336af1a35a681ba34e0177059c71c6f4380c3 100644 (file)
--- a/matita/components/thread/.depend
+++ b/matita/components/thread/.depend
@@ -1,6 +1,6 @@
-threadSafe.cmi:
-extThread.cmi:
-threadSafe.cmo: threadSafe.cmi
-threadSafe.cmx: threadSafe.cmi
-extThread.cmo: extThread.cmi
-extThread.cmx: extThread.cmi
+threadSafe.cmi :
+extThread.cmi :
+threadSafe.cmo : threadSafe.cmi
+threadSafe.cmx : threadSafe.cmi
+extThread.cmo : extThread.cmi
+extThread.cmx : extThread.cmi

diff --git a/matita/components/xml/.depend b/matita/components/xml/.depend
index eda62779ff37dd14feca9e54c864e5ebbd2b7b70..fd3f626b9b5ccd97b800d84a81bba82e49aa134c 100644 (file)
--- a/matita/components/xml/.depend
+++ b/matita/components/xml/.depend
@@ -1,6 +1,6 @@
-xml.cmi:
-xmlPushParser.cmi:
-xml.cmo: xml.cmi
-xml.cmx: xml.cmi
-xmlPushParser.cmo: xmlPushParser.cmi
-xmlPushParser.cmx: xmlPushParser.cmi
+xml.cmi :
+xmlPushParser.cmi :
+xml.cmo : xml.cmi
+xml.cmx : xml.cmi
+xmlPushParser.cmo : xmlPushParser.cmi
+xmlPushParser.cmx : xmlPushParser.cmi

diff --git a/matita/matita/.depend b/matita/matita/.depend
index 80fb425b03eb7f578aa3f68bd94115086d8bb78a..6c16e0b6e3158c39b22dec97404a39476ce4b6c2 100644 (file)
--- a/matita/matita/.depend
+++ b/matita/matita/.depend
@@ -1,78 +1,78 @@
-applyTransformation.cmo: applyTransformation.cmi
-applyTransformation.cmx: applyTransformation.cmi
-buildTimeConf.cmo:
-buildTimeConf.cmx:
-cicMathView.cmo: matitaMisc.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi \
+applyTransformation.cmo : applyTransformation.cmi
+applyTransformation.cmx : applyTransformation.cmi
+buildTimeConf.cmo :
+buildTimeConf.cmx :
+cicMathView.cmo : matitaMisc.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi \
     buildTimeConf.cmo applyTransformation.cmi cicMathView.cmi
-cicMathView.cmx: matitaMisc.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx \
+cicMathView.cmx : matitaMisc.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx \
     buildTimeConf.cmx applyTransformation.cmx cicMathView.cmi
-lablGraphviz.cmo: lablGraphviz.cmi
-lablGraphviz.cmx: lablGraphviz.cmi
-matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi
-matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi
-matitac.cmo: matitaclean.cmi matitaMisc.cmi matitaInit.cmi matitaExcPp.cmi \
+lablGraphviz.cmo : lablGraphviz.cmi
+lablGraphviz.cmx : lablGraphviz.cmi
+matitaclean.cmo : matitaMisc.cmi matitaInit.cmi matitaclean.cmi
+matitaclean.cmx : matitaMisc.cmx matitaInit.cmx matitaclean.cmi
+matitac.cmo : matitaclean.cmi matitaMisc.cmi matitaInit.cmi matitaExcPp.cmi \
     matitaEngine.cmi
-matitac.cmx: matitaclean.cmx matitaMisc.cmx matitaInit.cmx matitaExcPp.cmx \
+matitac.cmx : matitaclean.cmx matitaMisc.cmx matitaInit.cmx matitaExcPp.cmx \
     matitaEngine.cmx
-matitaEngine.cmo: applyTransformation.cmi matitaEngine.cmi
-matitaEngine.cmx: applyTransformation.cmx matitaEngine.cmi
-matitaExcPp.cmo: matitaEngine.cmi matitaExcPp.cmi
-matitaExcPp.cmx: matitaEngine.cmx matitaExcPp.cmi
-matitaGeneratedGui.cmo:
-matitaGeneratedGui.cmx:
-matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmo buildTimeConf.cmo \
+matitaEngine.cmo : applyTransformation.cmi matitaEngine.cmi
+matitaEngine.cmx : applyTransformation.cmx matitaEngine.cmi
+matitaExcPp.cmo : matitaEngine.cmi matitaExcPp.cmi
+matitaExcPp.cmx : matitaEngine.cmx matitaExcPp.cmi
+matitaGeneratedGui.cmo :
+matitaGeneratedGui.cmx :
+matitaGtkMisc.cmo : matitaTypes.cmi matitaGeneratedGui.cmo buildTimeConf.cmo \
     matitaGtkMisc.cmi
-matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx buildTimeConf.cmx \
+matitaGtkMisc.cmx : matitaTypes.cmx matitaGeneratedGui.cmx buildTimeConf.cmx \
     matitaGtkMisc.cmi
-matitaGui.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \
+matitaGui.cmo : matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \
     matitaMathView.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi \
     matitaGeneratedGui.cmo matitaExcPp.cmi buildTimeConf.cmo matitaGui.cmi
-matitaGui.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \
+matitaGui.cmx : matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \
     matitaMathView.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx \
     matitaGeneratedGui.cmx matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi
-matitaInit.cmo: matitaExcPp.cmi buildTimeConf.cmo matitaInit.cmi
-matitaInit.cmx: matitaExcPp.cmx buildTimeConf.cmx matitaInit.cmi
-matitaMathView.cmo: virtuals.cmi matitaTypes.cmi matitaMisc.cmi \
+matitaInit.cmo : matitaExcPp.cmi buildTimeConf.cmo matitaInit.cmi
+matitaInit.cmx : matitaExcPp.cmx buildTimeConf.cmx matitaInit.cmi
+matitaMathView.cmo : virtuals.cmi matitaTypes.cmi matitaMisc.cmi \
     matitaGuiTypes.cmi matitaGtkMisc.cmi matitaGeneratedGui.cmo \
     matitaExcPp.cmi lablGraphviz.cmi cicMathView.cmi buildTimeConf.cmo \
     applyTransformation.cmi matitaMathView.cmi
-matitaMathView.cmx: virtuals.cmx matitaTypes.cmx matitaMisc.cmx \
+matitaMathView.cmx : virtuals.cmx matitaTypes.cmx matitaMisc.cmx \
     matitaGuiTypes.cmi matitaGtkMisc.cmx matitaGeneratedGui.cmx \
     matitaExcPp.cmx lablGraphviz.cmx cicMathView.cmx buildTimeConf.cmx \
     applyTransformation.cmx matitaMathView.cmi
-matitaMisc.cmo: matitaGuiTypes.cmi buildTimeConf.cmo matitaMisc.cmi
-matitaMisc.cmx: matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi
-matita.cmo: predefined_virtuals.cmi matitaScript.cmi matitaMisc.cmi \
+matitaMisc.cmo : matitaGuiTypes.cmi buildTimeConf.cmo matitaMisc.cmi
+matitaMisc.cmx : matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi
+matita.cmo : predefined_virtuals.cmi matitaScript.cmi matitaMisc.cmi \
     matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmo \
     applyTransformation.cmi
-matita.cmx: predefined_virtuals.cmx matitaScript.cmx matitaMisc.cmx \
+matita.cmx : predefined_virtuals.cmx matitaScript.cmx matitaMisc.cmx \
     matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx \
     applyTransformation.cmx
-matitaScript.cmo: virtuals.cmi matitaTypes.cmi matitaMisc.cmi \
+matitaScript.cmo : virtuals.cmi matitaTypes.cmi matitaMisc.cmi \
     matitaMathView.cmi matitaGtkMisc.cmi matitaEngine.cmi cicMathView.cmi \
     buildTimeConf.cmo matitaScript.cmi
-matitaScript.cmx: virtuals.cmx matitaTypes.cmx matitaMisc.cmx \
+matitaScript.cmx : virtuals.cmx matitaTypes.cmx matitaMisc.cmx \
     matitaMathView.cmx matitaGtkMisc.cmx matitaEngine.cmx cicMathView.cmx \
     buildTimeConf.cmx matitaScript.cmi
-matitaTypes.cmo: matitaTypes.cmi
-matitaTypes.cmx: matitaTypes.cmi
-predefined_virtuals.cmo: virtuals.cmi predefined_virtuals.cmi
-predefined_virtuals.cmx: virtuals.cmx predefined_virtuals.cmi
-virtuals.cmo: virtuals.cmi
-virtuals.cmx: virtuals.cmi
-applyTransformation.cmi:
-cicMathView.cmi: matitaGuiTypes.cmi applyTransformation.cmi
-lablGraphviz.cmi:
-matitaclean.cmi:
-matitaEngine.cmi: applyTransformation.cmi
-matitaExcPp.cmi:
-matitaGtkMisc.cmi: matitaGeneratedGui.cmo
-matitaGui.cmi: matitaGuiTypes.cmi
-matitaGuiTypes.cmi: matitaGeneratedGui.cmo applyTransformation.cmi
-matitaInit.cmi:
-matitaMathView.cmi: matitaTypes.cmi matitaGuiTypes.cmi
-matitaMisc.cmi: matitaGuiTypes.cmi
-matitaScript.cmi:
-matitaTypes.cmi:
-predefined_virtuals.cmi:
-virtuals.cmi:
+matitaTypes.cmo : matitaTypes.cmi
+matitaTypes.cmx : matitaTypes.cmi
+predefined_virtuals.cmo : virtuals.cmi predefined_virtuals.cmi
+predefined_virtuals.cmx : virtuals.cmx predefined_virtuals.cmi
+virtuals.cmo : virtuals.cmi
+virtuals.cmx : virtuals.cmi
+applyTransformation.cmi :
+cicMathView.cmi : matitaGuiTypes.cmi applyTransformation.cmi
+lablGraphviz.cmi :
+matitaclean.cmi :
+matitaEngine.cmi : applyTransformation.cmi
+matitaExcPp.cmi :
+matitaGtkMisc.cmi : matitaGeneratedGui.cmo
+matitaGui.cmi : matitaGuiTypes.cmi
+matitaGuiTypes.cmi : matitaGeneratedGui.cmo applyTransformation.cmi
+matitaInit.cmi :
+matitaMathView.cmi : matitaTypes.cmi matitaGuiTypes.cmi
+matitaMisc.cmi : matitaGuiTypes.cmi
+matitaScript.cmi :
+matitaTypes.cmi :
+predefined_virtuals.cmi :
+virtuals.cmi :

diff --git a/matita/matita/.depend.opt b/matita/matita/.depend.opt
index be904cca8ae9a12fc00cb1f55964a0133b2c05d7..2df44877378e1f8703b80b2bfdb4b4ad3b354e43 100644 (file)
--- a/matita/matita/.depend.opt
+++ b/matita/matita/.depend.opt
@@ -18,24 +18,28 @@ matitaEngine.cmo : applyTransformation.cmi matitaEngine.cmi
 matitaEngine.cmx : applyTransformation.cmx matitaEngine.cmi
 matitaExcPp.cmo : matitaEngine.cmi matitaExcPp.cmi
 matitaExcPp.cmx : matitaEngine.cmx matitaExcPp.cmi
-matitaGtkMisc.cmo : matitaTypes.cmi buildTimeConf.cmx matitaGtkMisc.cmi
-matitaGtkMisc.cmx : matitaTypes.cmx buildTimeConf.cmx matitaGtkMisc.cmi
+matitaGeneratedGui.cmo :
+matitaGeneratedGui.cmx :
+matitaGtkMisc.cmo : matitaTypes.cmi matitaGeneratedGui.cmx buildTimeConf.cmx \
+    matitaGtkMisc.cmi
+matitaGtkMisc.cmx : matitaTypes.cmx matitaGeneratedGui.cmx buildTimeConf.cmx \
+    matitaGtkMisc.cmi
 matitaGui.cmo : matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \
-    matitaMathView.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi \
-    buildTimeConf.cmx matitaGui.cmi
+    matitaMathView.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi \
+    matitaGeneratedGui.cmx matitaExcPp.cmi buildTimeConf.cmx matitaGui.cmi
 matitaGui.cmx : matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \
-    matitaMathView.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx matitaExcPp.cmx \
-    buildTimeConf.cmx matitaGui.cmi
+    matitaMathView.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx \
+    matitaGeneratedGui.cmx matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi
 matitaInit.cmo : matitaExcPp.cmi buildTimeConf.cmx matitaInit.cmi
 matitaInit.cmx : matitaExcPp.cmx buildTimeConf.cmx matitaInit.cmi
 matitaMathView.cmo : virtuals.cmi matitaTypes.cmi matitaMisc.cmi \
-    matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi lablGraphviz.cmi \
-    cicMathView.cmi buildTimeConf.cmx applyTransformation.cmi \
-    matitaMathView.cmi
+    matitaGuiTypes.cmi matitaGtkMisc.cmi matitaGeneratedGui.cmx \
+    matitaExcPp.cmi lablGraphviz.cmi cicMathView.cmi buildTimeConf.cmx \
+    applyTransformation.cmi matitaMathView.cmi
 matitaMathView.cmx : virtuals.cmx matitaTypes.cmx matitaMisc.cmx \
-    matitaGuiTypes.cmi matitaGtkMisc.cmx matitaExcPp.cmx lablGraphviz.cmx \
-    cicMathView.cmx buildTimeConf.cmx applyTransformation.cmx \
-    matitaMathView.cmi
+    matitaGuiTypes.cmi matitaGtkMisc.cmx matitaGeneratedGui.cmx \
+    matitaExcPp.cmx lablGraphviz.cmx cicMathView.cmx buildTimeConf.cmx \
+    applyTransformation.cmx matitaMathView.cmi
 matitaMisc.cmo : matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi
 matitaMisc.cmx : matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi
 matita.cmo : predefined_virtuals.cmi matitaScript.cmi matitaMisc.cmi \
@@ -62,9 +66,9 @@ lablGraphviz.cmi :
 matitaclean.cmi :
 matitaEngine.cmi : applyTransformation.cmi
 matitaExcPp.cmi :
-matitaGtkMisc.cmi :
+matitaGtkMisc.cmi : matitaGeneratedGui.cmx
 matitaGui.cmi : matitaGuiTypes.cmi
-matitaGuiTypes.cmi : applyTransformation.cmi
+matitaGuiTypes.cmi : matitaGeneratedGui.cmx applyTransformation.cmi
 matitaInit.cmi :
 matitaMathView.cmi : matitaTypes.cmi matitaGuiTypes.cmi
 matitaMisc.cmi : matitaGuiTypes.cmi

diff --git a/matita/matita/matita.lang b/matita/matita/matita.lang
index 713b71810aef6ba0b74cdfd911007ce4efc053e6..ea9a08e1337cfffc3df116bc0ca487bab177abec 100644 (file)
--- a/matita/matita/matita.lang
+++ b/matita/matita/matita.lang
@@ -75,6 +75,9 @@
        <!-- Flow control & common keywords -->
        <context id="keywords" style-ref="keyword">
 
+        <!-- source -->
+         <keyword>implied</keyword>
+
         <!-- objects -->
          <keyword>theorem</keyword>
          <keyword>record</keyword>