From b6ceb877c05d27705ef163488aee38e60a86886c Mon Sep 17 00:00:00 2001 From: Andrea Berlingieri Date: Wed, 13 Mar 2019 23:18:13 +0100 Subject: [PATCH] Partially restore the assume tactic Add a type for the assume tactic in GrafiteAst Add pretty printing code for the assume tactic Add a parsing rule for the assume tactic in GrafiteParser Add a call in to the assume tactic in GrafiteEngine Add a file for the declarative tactics to the ng_tactics module Add code for the assume tactic in Declarative Add syntax highlight tag for the assume tactic Add the exact_tac signature to the interface file of nTactics --- matita/components/content/.depend.opt | 13 +++- matita/components/content_pres/.depend.opt | 46 ++++++++---- matita/components/disambiguation/.depend.opt | 10 ++- matita/components/extlib/.depend.opt | 31 +++++--- matita/components/getter/.depend.opt | 49 ++++++++----- matita/components/grafite/.depend.opt | 4 +- matita/components/grafite/grafiteAst.ml | 2 + matita/components/grafite/grafiteAstPp.ml | 1 + matita/components/grafite_engine/.depend.opt | 12 ++- .../grafite_engine/grafiteEngine.ml | 1 + matita/components/grafite_parser/.depend.opt | 6 +- .../grafite_parser/grafiteParser.ml | 1 + matita/components/library/.depend.opt | 9 ++- matita/components/logger/.depend.opt | 3 +- matita/components/ng_cic_content/.depend.opt | 6 +- .../components/ng_disambiguation/.depend.opt | 17 +++-- matita/components/ng_extraction/.depend.opt | 39 ++++++---- matita/components/ng_kernel/.depend.opt | 48 ++++++++---- matita/components/ng_library/.depend.opt | 3 +- .../components/ng_paramodulation/.depend.opt | 58 +++++++++------ matita/components/ng_refiner/.depend.opt | 32 +++++--- matita/components/ng_tactics/.depend.opt | 36 ++++++--- matita/components/ng_tactics/Makefile | 1 + matita/components/ng_tactics/declarative.ml | 30 ++++++++ matita/components/ng_tactics/declarative.mli | 26 +++++++ matita/components/ng_tactics/nTactics.mli | 2 + matita/components/registry/.depend.opt | 3 +- matita/components/syntax_extensions/.depend | 4 +- .../components/syntax_extensions/.depend.opt | 4 +- matita/components/thread/.depend.opt | 6 +- matita/components/xml/.depend.opt | 6 +- matita/matita/.depend.opt | 73 +++++++++++++------ matita/matita/matita.lang | 1 + 33 files changed, 411 insertions(+), 172 deletions(-) create mode 100644 matita/components/ng_tactics/declarative.ml create mode 100644 matita/components/ng_tactics/declarative.mli diff --git a/matita/components/content/.depend.opt b/matita/components/content/.depend.opt index 9c0b365c6..7bb00ba9b 100644 --- a/matita/components/content/.depend.opt +++ b/matita/components/content/.depend.opt @@ -1,9 +1,14 @@ -content.cmx : content.cmi content.cmi : -notationEnv.cmx : notationUtil.cmx notationPt.cmx notationEnv.cmi +notationUtil.cmi : notationPt.cmx notationEnv.cmi : notationPt.cmx -notationPp.cmx : notationPt.cmx notationEnv.cmx notationPp.cmi notationPp.cmi : notationPt.cmx notationEnv.cmi +notationPt.cmo : notationPt.cmx : +content.cmo : content.cmi +content.cmx : content.cmi +notationUtil.cmo : notationPt.cmx notationUtil.cmi notationUtil.cmx : notationPt.cmx notationUtil.cmi -notationUtil.cmi : notationPt.cmx +notationEnv.cmo : notationUtil.cmi notationPt.cmx notationEnv.cmi +notationEnv.cmx : notationUtil.cmx notationPt.cmx notationEnv.cmi +notationPp.cmo : notationPt.cmx notationEnv.cmi notationPp.cmi +notationPp.cmx : notationPt.cmx notationEnv.cmx notationPp.cmi diff --git a/matita/components/content_pres/.depend.opt b/matita/components/content_pres/.depend.opt index 211b4fc51..4deb6e591 100644 --- a/matita/components/content_pres/.depend.opt +++ b/matita/components/content_pres/.depend.opt @@ -1,24 +1,38 @@ -box.cmx : renderingAttrs.cmx box.cmi +renderingAttrs.cmi : +cicNotationLexer.cmi : +cicNotationParser.cmi : +mpresentation.cmi : box.cmi : -boxPp.cmx : renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx box.cmx \ - boxPp.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 -cicNotationLexer.cmi : +cicNotationParser.cmo : cicNotationLexer.cmi cicNotationParser.cmi cicNotationParser.cmx : cicNotationLexer.cmx cicNotationParser.cmi -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 \ + cicNotationParser.cmx termContentPres.cmi +boxPp.cmo : renderingAttrs.cmi mpresentation.cmi cicNotationPres.cmi box.cmi \ + boxPp.cmi +boxPp.cmx : renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx box.cmx \ + boxPp.cmi +cicNotationPres.cmo : renderingAttrs.cmi mpresentation.cmi box.cmi \ + cicNotationPres.cmi cicNotationPres.cmx : renderingAttrs.cmx mpresentation.cmx box.cmx \ cicNotationPres.cmi -cicNotationPres.cmi : mpresentation.cmi box.cmi +content2pres.cmo : termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \ + cicNotationPres.cmi box.cmi content2pres.cmi content2pres.cmx : termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \ cicNotationPres.cmx box.cmx content2pres.cmi -content2pres.cmi : termContentPres.cmi cicNotationPres.cmi -content2presMatcher.cmx : content2presMatcher.cmi -content2presMatcher.cmi : -mpresentation.cmx : mpresentation.cmi -mpresentation.cmi : -renderingAttrs.cmx : renderingAttrs.cmi -renderingAttrs.cmi : -termContentPres.cmx : renderingAttrs.cmx content2presMatcher.cmx \ - cicNotationParser.cmx termContentPres.cmi -termContentPres.cmi : cicNotationParser.cmi diff --git a/matita/components/disambiguation/.depend.opt b/matita/components/disambiguation/.depend.opt index 1f1711ae7..735bea7f7 100644 --- a/matita/components/disambiguation/.depend.opt +++ b/matita/components/disambiguation/.depend.opt @@ -1,7 +1,11 @@ -disambiguate.cmx : disambiguateTypes.cmx disambiguate.cmi +disambiguateTypes.cmi : disambiguate.cmi : disambiguateTypes.cmi +multiPassDisambiguator.cmi : disambiguateTypes.cmi disambiguate.cmi +disambiguateTypes.cmo : disambiguateTypes.cmi disambiguateTypes.cmx : disambiguateTypes.cmi -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.cmi -multiPassDisambiguator.cmi : disambiguateTypes.cmi disambiguate.cmi diff --git a/matita/components/extlib/.depend.opt b/matita/components/extlib/.depend.opt index 12de49274..e7b0a3bc7 100644 --- a/matita/components/extlib/.depend.opt +++ b/matita/components/extlib/.depend.opt @@ -1,18 +1,27 @@ -componentsConf.cmx : componentsConf.cmi componentsConf.cmi : -discrimination_tree.cmx : trie.cmx hExtlib.cmx discrimination_tree.cmi +hExtlib.cmi : +hMarshal.cmi : +patternMatcher.cmi : +hLog.cmi : +trie.cmi : discrimination_tree.cmi : -graphvizPp.cmx : graphvizPp.cmi +hTopoSort.cmi : graphvizPp.cmi : +componentsConf.cmo : componentsConf.cmi +componentsConf.cmx : componentsConf.cmi +hExtlib.cmo : hExtlib.cmi hExtlib.cmx : hExtlib.cmi -hExtlib.cmi : -hLog.cmx : hLog.cmi -hLog.cmi : +hMarshal.cmo : hExtlib.cmi hMarshal.cmi hMarshal.cmx : hExtlib.cmx hMarshal.cmi -hMarshal.cmi : -hTopoSort.cmx : hTopoSort.cmi -hTopoSort.cmi : +patternMatcher.cmo : patternMatcher.cmi patternMatcher.cmx : patternMatcher.cmi -patternMatcher.cmi : +hLog.cmo : hLog.cmi +hLog.cmx : hLog.cmi +trie.cmo : trie.cmi trie.cmx : trie.cmi -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.opt b/matita/components/getter/.depend.opt index 1d016d277..7c2b60586 100644 --- a/matita/components/getter/.depend.opt +++ b/matita/components/getter/.depend.opt @@ -1,23 +1,38 @@ -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 -http_getter.cmi : http_getter_types.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_common.cmi : http_getter_types.cmx -http_getter_const.cmx : http_getter_const.cmi +http_getter_wget.cmi : +http_getter_logger.cmi : +http_getter_misc.cmi : http_getter_const.cmi : -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_env.cmi : http_getter_types.cmx +http_getter_storage.cmi : +http_getter_common.cmi : http_getter_types.cmx +http_getter.cmi : http_getter_types.cmx +http_getter_types.cmo : +http_getter_types.cmx : +http_getter_wget.cmo : http_getter_types.cmx 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_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_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.cmx 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_logger.cmx http_getter_const.cmx http_getter_env.cmi +http_getter_storage.cmo : http_getter_wget.cmi http_getter_types.cmx \ + 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_misc.cmx http_getter_env.cmx http_getter_storage.cmi -http_getter_storage.cmi : -http_getter_types.cmx : -http_getter_wget.cmx : http_getter_types.cmx http_getter_wget.cmi -http_getter_wget.cmi : +http_getter_common.cmo : http_getter_types.cmx 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_logger.cmx http_getter_env.cmx http_getter_common.cmi +http_getter.cmo : http_getter_wget.cmi http_getter_types.cmx \ + 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_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.opt b/matita/components/grafite/.depend.opt index 5dabb8012..4a1ca42e9 100644 --- a/matita/components/grafite/.depend.opt +++ b/matita/components/grafite/.depend.opt @@ -1,3 +1,5 @@ +grafiteAstPp.cmi : grafiteAst.cmx +grafiteAst.cmo : grafiteAst.cmx : +grafiteAstPp.cmo : grafiteAst.cmx grafiteAstPp.cmi grafiteAstPp.cmx : grafiteAst.cmx grafiteAstPp.cmi -grafiteAstPp.cmi : grafiteAst.cmx diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml index 5d138bbe0..8b911a601 100644 --- a/matita/components/grafite/grafiteAst.ml +++ b/matita/components/grafite/grafiteAst.ml @@ -75,6 +75,8 @@ type ntactic = | NAssumption of loc | NRepeat of loc * ntactic | NBlock of loc * ntactic list + (* Declarative langauge *) + | Assume of loc * string * nterm (* loc, identifier, term *) type nmacro = | NCheck of loc * nterm diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml index 92944aaeb..d56e95de0 100644 --- a/matita/components/grafite/grafiteAstPp.ml +++ b/matita/components/grafite/grafiteAstPp.ml @@ -107,6 +107,7 @@ let rec pp_ntactic status ~map_unicode_to_tex = | NBlock (_,l) -> "(" ^ String.concat " " (List.map (pp_ntactic status ~map_unicode_to_tex) l)^ ")" | NRepeat (_,t) -> "nrepeat " ^ pp_ntactic status ~map_unicode_to_tex t + | Assume (_, ident, term) -> "assume" ^ ident ^ ":" ^ NotationPp.pp_term status term ;; let pp_nmacro status = function diff --git a/matita/components/grafite_engine/.depend.opt b/matita/components/grafite_engine/.depend.opt index 696b45881..e6d4942c6 100644 --- a/matita/components/grafite_engine/.depend.opt +++ b/matita/components/grafite_engine/.depend.opt @@ -1,7 +1,11 @@ -grafiteEngine.cmx : nCicCoercDeclaration.cmx grafiteTypes.cmx \ - grafiteEngine.cmi +grafiteTypes.cmi : +nCicCoercDeclaration.cmi : grafiteTypes.cmi grafiteEngine.cmi : grafiteTypes.cmi +grafiteTypes.cmo : grafiteTypes.cmi grafiteTypes.cmx : grafiteTypes.cmi -grafiteTypes.cmi : +nCicCoercDeclaration.cmo : grafiteTypes.cmi nCicCoercDeclaration.cmi nCicCoercDeclaration.cmx : grafiteTypes.cmx nCicCoercDeclaration.cmi -nCicCoercDeclaration.cmi : grafiteTypes.cmi +grafiteEngine.cmo : nCicCoercDeclaration.cmi grafiteTypes.cmi \ + grafiteEngine.cmi +grafiteEngine.cmx : nCicCoercDeclaration.cmx grafiteTypes.cmx \ + grafiteEngine.cmi diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index 387a09fe7..f76b8b02a 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -481,6 +481,7 @@ let eval_ng_tac tac = NTactics.block_tac (List.map (fun x -> aux f (text,prefix_len,x)) l) |GrafiteAst.NRepeat (_,tac) -> NTactics.repeat_tac (f f (text, prefix_len, tac)) + |GrafiteAst.Assume (_,id,t) -> Declarative.assume id t in aux aux tac (* trick for non uniform recursion call *) ;; diff --git a/matita/components/grafite_parser/.depend.opt b/matita/components/grafite_parser/.depend.opt index e0e6dac9c..752b0d88d 100644 --- a/matita/components/grafite_parser/.depend.opt +++ b/matita/components/grafite_parser/.depend.opt @@ -1,4 +1,6 @@ -grafiteParser.cmx : grafiteParser.cmi grafiteParser.cmi : -print_grammar.cmx : print_grammar.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 be39556d8..c1b347071 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -239,6 +239,7 @@ EXTEND | SYMBOL "#"; SYMBOL "_" -> G.NTactic(loc,[ G.NIntro (loc,"_")]) | SYMBOL "*" -> G.NTactic(loc,[ G.NCase1 (loc,"_")]) | SYMBOL "*"; "as"; n=IDENT -> G.NTactic(loc,[ G.NCase1 (loc,n)]) + | IDENT "assume"; id = IDENT; SYMBOL ":"; t = tactic_term -> G.NTactic (loc,[G.Assume (loc,id,t)]) ] ]; auto_fixed_param: [ diff --git a/matita/components/library/.depend.opt b/matita/components/library/.depend.opt index 27ecf9383..6f2769b94 100644 --- a/matita/components/library/.depend.opt +++ b/matita/components/library/.depend.opt @@ -1,6 +1,9 @@ -librarian.cmx : librarian.cmi librarian.cmi : -libraryClean.cmx : libraryClean.cmi +libraryMisc.cmi : libraryClean.cmi : +librarian.cmo : librarian.cmi +librarian.cmx : librarian.cmi +libraryMisc.cmo : libraryMisc.cmi libraryMisc.cmx : libraryMisc.cmi -libraryMisc.cmi : +libraryClean.cmo : libraryClean.cmi +libraryClean.cmx : libraryClean.cmi diff --git a/matita/components/logger/.depend.opt b/matita/components/logger/.depend.opt index ed934897f..d1b4c3716 100644 --- a/matita/components/logger/.depend.opt +++ b/matita/components/logger/.depend.opt @@ -1,2 +1,3 @@ -helmLogger.cmx : helmLogger.cmi helmLogger.cmi : +helmLogger.cmo : helmLogger.cmi +helmLogger.cmx : helmLogger.cmi diff --git a/matita/components/ng_cic_content/.depend.opt b/matita/components/ng_cic_content/.depend.opt index df8d6d635..01e2f5b1e 100644 --- a/matita/components/ng_cic_content/.depend.opt +++ b/matita/components/ng_cic_content/.depend.opt @@ -1,4 +1,6 @@ -interpretations.cmx : ncic2astMatcher.cmx interpretations.cmi +ncic2astMatcher.cmi : interpretations.cmi : +ncic2astMatcher.cmo : ncic2astMatcher.cmi ncic2astMatcher.cmx : ncic2astMatcher.cmi -ncic2astMatcher.cmi : +interpretations.cmo : ncic2astMatcher.cmi interpretations.cmi +interpretations.cmx : ncic2astMatcher.cmx interpretations.cmi diff --git a/matita/components/ng_disambiguation/.depend.opt b/matita/components/ng_disambiguation/.depend.opt index d5eef6bc0..79fd839b2 100644 --- a/matita/components/ng_disambiguation/.depend.opt +++ b/matita/components/ng_disambiguation/.depend.opt @@ -1,9 +1,14 @@ -disambiguateChoices.cmx : nnumber_notation.cmx disambiguateChoices.cmi +nnumber_notation.cmi : disambiguateChoices.cmi : -grafiteDisambiguate.cmx : nCicDisambiguate.cmx disambiguateChoices.cmx \ - grafiteDisambiguate.cmi -grafiteDisambiguate.cmi : -nCicDisambiguate.cmx : nCicDisambiguate.cmi nCicDisambiguate.cmi : +grafiteDisambiguate.cmi : +nnumber_notation.cmo : nnumber_notation.cmi nnumber_notation.cmx : nnumber_notation.cmi -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.cmi diff --git a/matita/components/ng_extraction/.depend.opt b/matita/components/ng_extraction/.depend.opt index 03f5f9a00..968d8ffe9 100644 --- a/matita/components/ng_extraction/.depend.opt +++ b/matita/components/ng_extraction/.depend.opt @@ -1,21 +1,34 @@ -common.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \ - common.cmi -common.cmi : ocamlExtractionTable.cmi mlutil.cmi miniml.cmx coq.cmi -coq.cmx : coq.cmi +nCicExtraction.cmi : coq.cmi : -extraction.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \ - common.cmx extraction.cmi +ocamlExtractionTable.cmi : miniml.cmx coq.cmi +mlutil.cmi : ocamlExtractionTable.cmi miniml.cmx coq.cmi +common.cmi : ocamlExtractionTable.cmi mlutil.cmi miniml.cmx coq.cmi extraction.cmi : ocamlExtractionTable.cmi miniml.cmx coq.cmi +ocaml.cmi : ocamlExtractionTable.cmi miniml.cmx coq.cmi +ocamlExtraction.cmi : ocamlExtractionTable.cmi +miniml.cmo : coq.cmi miniml.cmx : coq.cmx -mlutil.cmx : ocamlExtractionTable.cmx miniml.cmx coq.cmx mlutil.cmi -mlutil.cmi : ocamlExtractionTable.cmi miniml.cmx coq.cmi +nCicExtraction.cmo : nCicExtraction.cmi nCicExtraction.cmx : nCicExtraction.cmi -nCicExtraction.cmi : +coq.cmo : coq.cmi +coq.cmx : coq.cmi +ocamlExtractionTable.cmo : miniml.cmx coq.cmi ocamlExtractionTable.cmi +ocamlExtractionTable.cmx : miniml.cmx coq.cmx ocamlExtractionTable.cmi +mlutil.cmo : ocamlExtractionTable.cmi miniml.cmx coq.cmi mlutil.cmi +mlutil.cmx : ocamlExtractionTable.cmx miniml.cmx coq.cmx mlutil.cmi +common.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmx coq.cmi \ + common.cmi +common.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \ + common.cmi +extraction.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmx 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.cmx coq.cmi \ + common.cmi ocaml.cmi ocaml.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \ common.cmx ocaml.cmi -ocaml.cmi : ocamlExtractionTable.cmi miniml.cmx coq.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 -ocamlExtraction.cmi : ocamlExtractionTable.cmi -ocamlExtractionTable.cmx : miniml.cmx coq.cmx ocamlExtractionTable.cmi -ocamlExtractionTable.cmi : miniml.cmx coq.cmi diff --git a/matita/components/ng_kernel/.depend.opt b/matita/components/ng_kernel/.depend.opt index fe2e99a30..5b0507784 100644 --- a/matita/components/ng_kernel/.depend.opt +++ b/matita/components/ng_kernel/.depend.opt @@ -1,25 +1,41 @@ -nCic.cmx : nUri.cmx nReference.cmx -nCicEnvironment.cmx : nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi +nUri.cmi : +nReference.cmi : nUri.cmi +nCicUtils.cmi : nCic.cmx +nCicSubstitution.cmi : nCic.cmx nCicEnvironment.cmi : nUri.cmi nReference.cmi nCic.cmx -nCicPp.cmx : nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \ - nCicEnvironment.cmx nCic.cmx nCicPp.cmi -nCicPp.cmi : nReference.cmi nCic.cmx -nCicReduction.cmx : nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ - nCicEnvironment.cmx nCic.cmx nCicReduction.cmi nCicReduction.cmi : nCic.cmx +nCicTypeChecker.cmi : nUri.cmi nReference.cmi nCic.cmx +nCicUntrusted.cmi : nCic.cmx +nCicPp.cmi : nReference.cmi nCic.cmx +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.cmx nCicUtils.cmi +nCicUtils.cmx : nReference.cmx nCic.cmx nCicUtils.cmi +nCicSubstitution.cmo : nReference.cmi nCicUtils.cmi nCic.cmx \ + nCicSubstitution.cmi nCicSubstitution.cmx : nReference.cmx nCicUtils.cmx nCic.cmx \ nCicSubstitution.cmi -nCicSubstitution.cmi : nCic.cmx +nCicEnvironment.cmo : nUri.cmi nReference.cmi nCic.cmx nCicEnvironment.cmi +nCicEnvironment.cmx : nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi +nCicReduction.cmo : nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ + nCicEnvironment.cmi nCic.cmx nCicReduction.cmi +nCicReduction.cmx : nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ + nCicEnvironment.cmx nCic.cmx nCicReduction.cmi +nCicTypeChecker.cmo : nUri.cmi nReference.cmi nCicUtils.cmi \ + nCicSubstitution.cmi nCicReduction.cmi nCicEnvironment.cmi nCic.cmx \ + nCicTypeChecker.cmi nCicTypeChecker.cmx : nUri.cmx nReference.cmx nCicUtils.cmx \ nCicSubstitution.cmx nCicReduction.cmx nCicEnvironment.cmx nCic.cmx \ nCicTypeChecker.cmi -nCicTypeChecker.cmi : nUri.cmi nReference.cmi nCic.cmx +nCicUntrusted.cmo : nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ + nCicReduction.cmi nCicEnvironment.cmi nCic.cmx nCicUntrusted.cmi nCicUntrusted.cmx : nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ nCicReduction.cmx nCicEnvironment.cmx nCic.cmx nCicUntrusted.cmi -nCicUntrusted.cmi : nCic.cmx -nCicUtils.cmx : nReference.cmx nCic.cmx nCicUtils.cmi -nCicUtils.cmi : nCic.cmx -nReference.cmx : nUri.cmx nReference.cmi -nReference.cmi : nUri.cmi -nUri.cmx : nUri.cmi -nUri.cmi : +nCicPp.cmo : nUri.cmi nReference.cmi nCicSubstitution.cmi nCicReduction.cmi \ + nCicEnvironment.cmi nCic.cmx nCicPp.cmi +nCicPp.cmx : nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \ + nCicEnvironment.cmx nCic.cmx nCicPp.cmi diff --git a/matita/components/ng_library/.depend.opt b/matita/components/ng_library/.depend.opt index 07d53f5dd..a571a865c 100644 --- a/matita/components/ng_library/.depend.opt +++ b/matita/components/ng_library/.depend.opt @@ -1,2 +1,3 @@ -nCicLibrary.cmx : nCicLibrary.cmi nCicLibrary.cmi : +nCicLibrary.cmo : nCicLibrary.cmi +nCicLibrary.cmx : nCicLibrary.cmi diff --git a/matita/components/ng_paramodulation/.depend.opt b/matita/components/ng_paramodulation/.depend.opt index 6e58a4ca9..5f4f1cc56 100644 --- a/matita/components/ng_paramodulation/.depend.opt +++ b/matita/components/ng_paramodulation/.depend.opt @@ -1,29 +1,45 @@ -foSubst.cmx : terms.cmx foSubst.cmi +terms.cmi : +pp.cmi : terms.cmi foSubst.cmi : terms.cmi -foUnif.cmx : terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi -foUnif.cmi : terms.cmi orderings.cmi -foUtils.cmx : terms.cmx orderings.cmx foSubst.cmx foUtils.cmi +orderings.cmi : terms.cmi foUtils.cmi : terms.cmi orderings.cmi -index.cmx : terms.cmx pp.cmx orderings.cmx foUtils.cmx foUnif.cmx index.cmi +foUnif.cmi : terms.cmi orderings.cmi index.cmi : terms.cmi orderings.cmi -nCicBlob.cmx : terms.cmx foUtils.cmx nCicBlob.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 -nCicParamod.cmx : terms.cmx pp.cmx paramod.cmx orderings.cmx nCicProof.cmx \ - nCicBlob.cmx nCicParamod.cmi -nCicParamod.cmi : terms.cmi -nCicProof.cmx : terms.cmx pp.cmx nCicBlob.cmx foSubst.cmx nCicProof.cmi nCicProof.cmi : terms.cmi -orderings.cmx : terms.cmx pp.cmx foSubst.cmx orderings.cmi -orderings.cmi : terms.cmi -paramod.cmx : terms.cmx superposition.cmx pp.cmx orderings.cmx index.cmx \ - foUtils.cmx foUnif.cmx paramod.cmi -paramod.cmi : terms.cmi orderings.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 -pp.cmi : terms.cmi -stats.cmx : terms.cmx stats.cmi -stats.cmi : terms.cmi orderings.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 \ foUnif.cmx foSubst.cmx superposition.cmi -superposition.cmi : terms.cmi orderings.cmi index.cmi -terms.cmx : terms.cmi -terms.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 \ + 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.cmi nCicParamod.cmi +nCicParamod.cmx : terms.cmx pp.cmx paramod.cmx orderings.cmx nCicProof.cmx \ + nCicBlob.cmx nCicParamod.cmi diff --git a/matita/components/ng_refiner/.depend.opt b/matita/components/ng_refiner/.depend.opt index dab873890..d8295760a 100644 --- a/matita/components/ng_refiner/.depend.opt +++ b/matita/components/ng_refiner/.depend.opt @@ -1,17 +1,27 @@ -nCicCoercion.cmx : nDiscriminationTree.cmx nCicUnifHint.cmx \ - nCicMetaSubst.cmx nCicCoercion.cmi -nCicCoercion.cmi : nCicUnifHint.cmi -nCicMetaSubst.cmx : nCicMetaSubst.cmi +nDiscriminationTree.cmi : nCicMetaSubst.cmi : -nCicRefineUtil.cmx : nCicMetaSubst.cmx nCicRefineUtil.cmi +nCicUnifHint.cmi : +nCicCoercion.cmi : nCicUnifHint.cmi nCicRefineUtil.cmi : -nCicRefiner.cmx : nCicUnification.cmx nCicRefineUtil.cmx nCicMetaSubst.cmx \ - nCicCoercion.cmx nCicRefiner.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 -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 -nCicUnification.cmi : nCicCoercion.cmi -nDiscriminationTree.cmx : nDiscriminationTree.cmi -nDiscriminationTree.cmi : +nCicRefiner.cmo : nCicUnification.cmi nCicRefineUtil.cmi nCicMetaSubst.cmi \ + nCicCoercion.cmi nCicRefiner.cmi +nCicRefiner.cmx : nCicUnification.cmx nCicRefineUtil.cmx nCicMetaSubst.cmx \ + nCicCoercion.cmx nCicRefiner.cmi diff --git a/matita/components/ng_tactics/.depend.opt b/matita/components/ng_tactics/.depend.opt index c8999df5a..420a5dbc6 100644 --- a/matita/components/ng_tactics/.depend.opt +++ b/matita/components/ng_tactics/.depend.opt @@ -1,19 +1,33 @@ -continuationals.cmx : continuationals.cmi continuationals.cmi : -nCicElim.cmx : nCicElim.cmi -nCicElim.cmi : -nCicTacReduction.cmx : nCicTacReduction.cmi nCicTacReduction.cmi : -nDestructTac.cmx : nTactics.cmx nTacStatus.cmx continuationals.cmx \ - nDestructTac.cmi +nTacStatus.cmi : continuationals.cmi +nCicElim.cmi : +nTactics.cmi : nTacStatus.cmi +declarative.cmi : nTacStatus.cmi +nnAuto.cmi : nTacStatus.cmi nDestructTac.cmi : nTacStatus.cmi -nInversion.cmx : nTactics.cmx nTacStatus.cmx nCicElim.cmx \ - continuationals.cmx nInversion.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 -nTacStatus.cmi : continuationals.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 -nTactics.cmi : nTacStatus.cmi +declarative.cmo : nTactics.cmi declarative.cmi +declarative.cmx : nTactics.cmx declarative.cmi +nnAuto.cmo : nTactics.cmi nTacStatus.cmi nCicTacReduction.cmi \ + continuationals.cmi nnAuto.cmi nnAuto.cmx : nTactics.cmx nTacStatus.cmx nCicTacReduction.cmx \ continuationals.cmx nnAuto.cmi -nnAuto.cmi : nTacStatus.cmi +nDestructTac.cmo : nTactics.cmi nTacStatus.cmi continuationals.cmi \ + nDestructTac.cmi +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 diff --git a/matita/components/ng_tactics/Makefile b/matita/components/ng_tactics/Makefile index 3a261d192..c9b82e044 100644 --- a/matita/components/ng_tactics/Makefile +++ b/matita/components/ng_tactics/Makefile @@ -6,6 +6,7 @@ INTERFACE_FILES = \ nTacStatus.mli \ nCicElim.mli \ nTactics.mli \ + declarative.mli \ nnAuto.mli \ nDestructTac.mli \ nInversion.mli diff --git a/matita/components/ng_tactics/declarative.ml b/matita/components/ng_tactics/declarative.ml new file mode 100644 index 000000000..532ffbb37 --- /dev/null +++ b/matita/components/ng_tactics/declarative.ml @@ -0,0 +1,30 @@ +(* Copyright (C) 2019, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +module Ast = NotationPt +open NTactics + +let assume name ty = + exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (name,None),Some ty),Ast.Implicit `JustOne))) diff --git a/matita/components/ng_tactics/declarative.mli b/matita/components/ng_tactics/declarative.mli new file mode 100644 index 000000000..f6f0ff953 --- /dev/null +++ b/matita/components/ng_tactics/declarative.mli @@ -0,0 +1,26 @@ +(* Copyright (C) 2019, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +val assume : string -> NotationPt.term -> 's NTacStatus.tactic diff --git a/matita/components/ng_tactics/nTactics.mli b/matita/components/ng_tactics/nTactics.mli index 5290a322e..c492b8c64 100644 --- a/matita/components/ng_tactics/nTactics.mli +++ b/matita/components/ng_tactics/nTactics.mli @@ -89,3 +89,5 @@ val find_in_context : 'a -> ('a * 'b) list -> int val inversion_tac: what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 's NTacStatus.tactic + +val exact_tac: NTacStatus.tactic_term -> 's NTacStatus.tactic diff --git a/matita/components/registry/.depend.opt b/matita/components/registry/.depend.opt index f28210446..67113e67f 100644 --- a/matita/components/registry/.depend.opt +++ b/matita/components/registry/.depend.opt @@ -1,2 +1,3 @@ -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/syntax_extensions/.depend b/matita/components/syntax_extensions/.depend index 8b3261bc8..4b9bcffd4 100644 --- a/matita/components/syntax_extensions/.depend +++ b/matita/components/syntax_extensions/.depend @@ -1,5 +1,5 @@ -utf8Macro.cmo : utf8MacroTable.cmo utf8Macro.cmi -utf8Macro.cmx : utf8MacroTable.cmx utf8Macro.cmi utf8Macro.cmi : utf8MacroTable.cmo : utf8MacroTable.cmx : +utf8Macro.cmo : utf8MacroTable.cmo utf8Macro.cmi +utf8Macro.cmx : utf8MacroTable.cmx utf8Macro.cmi diff --git a/matita/components/syntax_extensions/.depend.opt b/matita/components/syntax_extensions/.depend.opt index 98ac1d844..24f371ca7 100644 --- a/matita/components/syntax_extensions/.depend.opt +++ b/matita/components/syntax_extensions/.depend.opt @@ -1,3 +1,5 @@ -utf8Macro.cmx : utf8MacroTable.cmx utf8Macro.cmi utf8Macro.cmi : +utf8MacroTable.cmo : utf8MacroTable.cmx : +utf8Macro.cmo : utf8MacroTable.cmx utf8Macro.cmi +utf8Macro.cmx : utf8MacroTable.cmx utf8Macro.cmi diff --git a/matita/components/thread/.depend.opt b/matita/components/thread/.depend.opt index 8ee8dbbec..d68336af1 100644 --- a/matita/components/thread/.depend.opt +++ b/matita/components/thread/.depend.opt @@ -1,4 +1,6 @@ -extThread.cmx : extThread.cmi +threadSafe.cmi : extThread.cmi : +threadSafe.cmo : threadSafe.cmi threadSafe.cmx : threadSafe.cmi -threadSafe.cmi : +extThread.cmo : extThread.cmi +extThread.cmx : extThread.cmi diff --git a/matita/components/xml/.depend.opt b/matita/components/xml/.depend.opt index 36a543808..fd3f626b9 100644 --- a/matita/components/xml/.depend.opt +++ b/matita/components/xml/.depend.opt @@ -1,4 +1,6 @@ -xml.cmx : xml.cmi xml.cmi : -xmlPushParser.cmx : xmlPushParser.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.opt b/matita/matita/.depend.opt index 5c7d0715a..2df448773 100644 --- a/matita/matita/.depend.opt +++ b/matita/matita/.depend.opt @@ -1,47 +1,78 @@ +applyTransformation.cmo : applyTransformation.cmi applyTransformation.cmx : applyTransformation.cmi -applyTransformation.cmi : +buildTimeConf.cmo : buildTimeConf.cmx : +cicMathView.cmo : matitaMisc.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi \ + buildTimeConf.cmx applyTransformation.cmi cicMathView.cmi cicMathView.cmx : matitaMisc.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx \ buildTimeConf.cmx applyTransformation.cmx cicMathView.cmi -cicMathView.cmi : matitaGuiTypes.cmi applyTransformation.cmi +lablGraphviz.cmo : lablGraphviz.cmi lablGraphviz.cmx : lablGraphviz.cmi -lablGraphviz.cmi : -matita.cmx : predefined_virtuals.cmx matitaScript.cmx matitaMisc.cmx \ - matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx \ - applyTransformation.cmx +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 \ + matitaEngine.cmx +matitaEngine.cmo : applyTransformation.cmi matitaEngine.cmi matitaEngine.cmx : applyTransformation.cmx matitaEngine.cmi -matitaEngine.cmi : applyTransformation.cmi +matitaExcPp.cmo : matitaEngine.cmi matitaExcPp.cmi matitaExcPp.cmx : matitaEngine.cmx matitaExcPp.cmi -matitaExcPp.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 -matitaGtkMisc.cmi : matitaGeneratedGui.cmx +matitaGui.cmo : matitaTypes.cmi matitaScript.cmi matitaMisc.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 \ matitaGeneratedGui.cmx matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi -matitaGui.cmi : matitaGuiTypes.cmi -matitaGuiTypes.cmi : matitaGeneratedGui.cmx applyTransformation.cmi +matitaInit.cmo : matitaExcPp.cmi buildTimeConf.cmx matitaInit.cmi matitaInit.cmx : matitaExcPp.cmx buildTimeConf.cmx matitaInit.cmi -matitaInit.cmi : +matitaMathView.cmo : virtuals.cmi matitaTypes.cmi matitaMisc.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 matitaGeneratedGui.cmx \ matitaExcPp.cmx lablGraphviz.cmx cicMathView.cmx buildTimeConf.cmx \ applyTransformation.cmx matitaMathView.cmi -matitaMathView.cmi : matitaTypes.cmi matitaGuiTypes.cmi +matitaMisc.cmo : matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi matitaMisc.cmx : matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi -matitaMisc.cmi : matitaGuiTypes.cmi +matita.cmo : predefined_virtuals.cmi matitaScript.cmi matitaMisc.cmi \ + matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmx \ + applyTransformation.cmi +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 \ + matitaMathView.cmi matitaGtkMisc.cmi matitaEngine.cmi cicMathView.cmi \ + buildTimeConf.cmx matitaScript.cmi matitaScript.cmx : virtuals.cmx matitaTypes.cmx matitaMisc.cmx \ matitaMathView.cmx matitaGtkMisc.cmx matitaEngine.cmx cicMathView.cmx \ buildTimeConf.cmx matitaScript.cmi -matitaScript.cmi : +matitaTypes.cmo : matitaTypes.cmi matitaTypes.cmx : matitaTypes.cmi -matitaTypes.cmi : -matitac.cmx : matitaclean.cmx matitaMisc.cmx matitaInit.cmx matitaExcPp.cmx \ - matitaEngine.cmx -matitaclean.cmx : matitaMisc.cmx matitaInit.cmx matitaclean.cmi -matitaclean.cmi : +predefined_virtuals.cmo : virtuals.cmi predefined_virtuals.cmi predefined_virtuals.cmx : virtuals.cmx predefined_virtuals.cmi -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.cmx +matitaGui.cmi : matitaGuiTypes.cmi +matitaGuiTypes.cmi : matitaGeneratedGui.cmx 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/matita.lang b/matita/matita/matita.lang index 3caf034a3..8a47418b6 100644 --- a/matita/matita/matita.lang +++ b/matita/matita/matita.lang @@ -106,6 +106,7 @@ inversion lapply destruct + assume alias -- 2.39.2