From 6c15dd2d7c372dc163c24e96bf56376c5bcb5a6c Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 5 Sep 2015 15:14:26 +0000 Subject: [PATCH] - 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] --- matita/components/binaries/probe/options.mli | 2 +- matita/components/binaries/probe/probe.ml | 12 +- matita/components/content/.depend | 28 ++--- matita/components/content_pres/.depend | 60 +++++----- matita/components/disambiguation/.depend | 18 +-- matita/components/extlib/.depend | 54 ++++----- matita/components/getter/.depend | 52 ++++----- matita/components/grafite/.depend | 10 +- matita/components/grafite_engine/.depend | 18 +-- matita/components/grafite_parser/.depend | 12 +- .../grafite_parser/grafiteParser.ml | 36 +++--- matita/components/library/.depend | 18 +-- matita/components/logger/.depend | 6 +- matita/components/ng_cic_content/.depend | 12 +- matita/components/ng_disambiguation/.depend | 24 ++-- matita/components/ng_extraction/.depend | 34 ++++++ matita/components/ng_kernel/.depend | 58 +++++----- matita/components/ng_kernel/nCic.ml | 13 ++- matita/components/ng_kernel/nCicPp.ml | 1 + matita/components/ng_library/.depend | 6 +- matita/components/ng_paramodulation/.depend | 78 ++++++------- matita/components/ng_refiner/.depend | 48 ++++---- matita/components/ng_tactics/.depend | 52 ++++----- matita/components/registry/.depend | 6 +- matita/components/thread/.depend | 12 +- matita/components/xml/.depend | 12 +- matita/matita/.depend | 108 +++++++++--------- matita/matita/.depend.opt | 32 +++--- matita/matita/matita.lang | 3 + 29 files changed, 442 insertions(+), 383 deletions(-) create mode 100644 matita/components/ng_extraction/.depend diff --git a/matita/components/binaries/probe/options.mli b/matita/components/binaries/probe/options.mli index 3e9789c76..a692c9013 100644 --- 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 55b942cc1..748826be1 100644 --- 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 | | -gp | HELM (base)uri | -i | -on | os | -sn | -ss ]*" in + let help = "Usage: probe [ -X | | -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 0671b66fe..369dbbdc4 100644 --- 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 03a1732eb..4deb6e591 100644 --- 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 fa6388aa7..735bea7f7 100644 --- 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 b121fbcd1..e7b0a3bc7 100644 --- 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 600dc01db..59c0b896e 100644 --- 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 ba4fab03a..e70c83c77 100644 --- 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 27787b008..e6d4942c6 100644 --- 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 5142da1bf..752b0d88d 100644 --- 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 112970d3e..70fe2f415 100644 --- 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> (* ≝ *); 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> (* ≝ *); + | src = source; nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode> (* ≝ *); 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 28703386a..6f2769b94 100644 --- 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 1c8ec5b7c..d1b4c3716 100644 --- 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 b1a499fd3..01e2f5b1e 100644 --- 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 d5306074a..79fd839b2 100644 --- 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 index 000000000..c2ad6ff86 --- /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 16f0d02cc..a55f87284 100644 --- 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 94dc827c8..03672a0c4 100644 --- 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 11ba55e78..5a99a0664 100644 --- 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 b9e7731f9..a571a865c 100644 --- 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 4e9e21a19..5f4f1cc56 100644 --- 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 5e055ecdc..d8295760a 100644 --- 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 3e01ca0fb..e8ca8210e 100644 --- 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 19a1fd325..67113e67f 100644 --- 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 e25145b8b..d68336af1 100644 --- 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 eda62779f..fd3f626b9 100644 --- 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 80fb425b0..6c16e0b6e 100644 --- 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 be904cca8..2df448773 100644 --- 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 713b71810..ea9a08e13 100644 --- a/matita/matita/matita.lang +++ b/matita/matita/matita.lang @@ -75,6 +75,9 @@ + + implied + theorem record -- 2.39.2