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

diff --git a/matita/components/content/.depend.opt b/matita/components/content/.depend.opt
index 9c0b365c6a3ee363406a84761e14ee85ce710069..7bb00ba9b9ba6f280bb4ebbbe066b02343b3a08b 100644 (file)
--- 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 211b4fc51200e2b3cf63db3bf38852b77c370dda..4deb6e591a8c9b1118318f7a7264800d533fbece 100644 (file)
--- 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 1f1711ae7f14eaf50a6f86c6fc91f58a0c7ce4a1..735bea7f72c4ccf1beef11818a346a3d4c3d6e6a 100644 (file)
--- 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 12de49274a4db6fba23ff7191d8503ed1e943560..e7b0a3bc74142a75bb82718931527b2b33db82e2 100644 (file)
--- 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 1d016d277ad431861b42fafb78ffdd2011480674..7c2b605861ee7340a4908ed5d3085ccbc0a7d401 100644 (file)
--- 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 5dabb8012003194da1d473cc5a561e1d99bf65d2..4a1ca42e9e7b83203739006eb1df032ce7c8629d 100644 (file)
--- 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 5d138bbe06624ed27896cfb0511767ee045448a6..8b911a60183c1ff0a7022160056e5696e8ee9dee 100644 (file)
--- 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 92944aaebd5b102be15c0ea93f242e74bc40773f..d56e95de0cacafdcc8b4e785edc6b208c126516d 100644 (file)
--- 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 696b4588179e989a2ae83a739c57852e3d51d8f6..e6d4942c67b319e5e52866b737ef24ee4091860e 100644 (file)
--- 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 387a09fe78b86ea4542736f7e499726a5ead5454..f76b8b02a802e80a406e1d9b8321c47b5e2b9087 100644 (file)
--- 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 e0e6dac9c2dcb31f52f80b9b237789c528f048cf..752b0d88d5ca9ccf9f59da28b6578d37e2a58763 100644 (file)
--- 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 be39556d8502fb59826083c753232a1e60148107..c1b347071b799ce5ed9630f32ffc15672cd72b15 100644 (file)
--- 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 27ecf93835014baa578b3cd07a7cb09b8cb5a687..6f2769b943d3b17c0eaa88d03ff693cda70b64e2 100644 (file)
--- 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 ed934897fdbd39b817c5b6303e596f74dff221d2..d1b4c37162663daab85eee7845f39b2422456992 100644 (file)
--- 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 df8d6d6357841ca9eecfae3246d3df739c1c1f16..01e2f5b1ef6d52b1677f749f6a30ec2eb6ed65db 100644 (file)
--- 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 d5eef6bc06265d73f5d3443041b60c587a92931f..79fd839b24f42bc72c2f7a9221dfa9fc047acb37 100644 (file)
--- 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 03f5f9a002277b547522f2e78ba6bf18a21afeea..968d8ffe9355dad2b602be5a4861ee71b475fabb 100644 (file)
--- 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 fe2e99a30a19e52306717451f3e19f28c3269e36..5b05077847c163d3e2d4080466d09e98b971641a 100644 (file)
--- 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 07d53f5dd0b86ddb9d895e15e2c8914d08d5ceac..a571a865c12712184f2df7cb39b8afb4191c4cf5 100644 (file)
--- 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 6e58a4ca97e3980902a3a626518ab1b8284b8b2c..5f4f1cc562e40087cacaebc42ee367dc784ebae6 100644 (file)
--- 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 dab8738901678689b5c7753b5a95b2e45cf09bc4..d8295760aff118a07e4066718ff8146fb64f0228 100644 (file)
--- 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 c8999df5a2a69629233c9ad4d8ff3f228bd7f33f..420a5dbc6ab22514608d9e9578d7050f53692716 100644 (file)
--- 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 3a261d192563e716b87b8ab4b2a595ab657a5cb0..c9b82e04414f2ea25dc4276ae61e3b2e34c7c24e 100644 (file)
--- 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 (file)
index 0000000..532ffbb
--- /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 (file)
index 0000000..f6f0ff9
--- /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 5290a322e2db63e79a4209df396ee377e4d70927..c492b8c644c1279d2da38b78acd58ffecb4eb338 100644 (file)
--- 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 f282104465c4bc6d90927ebb77b2a2fe5e48e67f..67113e67f7af0c0d4e8e6ae696d91d217f620df6 100644 (file)
--- 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 8b3261bc8dffab9f1027b21f36125b37d79a49e2..4b9bcffd411bfa4af1b6e971d5e50079d8bc0af0 100644 (file)
--- 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 98ac1d844e00cb9bd07f41a86482f326bdaf4fb4..24f371ca742c7b4096f789b860086f44071a5f11 100644 (file)
--- 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 8ee8dbbec0891bf4392eaef92a3ed399c547a59a..d68336af1a35a681ba34e0177059c71c6f4380c3 100644 (file)
--- 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 36a5438084a6137a7f9158f4fc45a2e82c40d60d..fd3f626b9b5ccd97b800d84a81bba82e49aa134c 100644 (file)
--- 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 5c7d0715ae4df145104d4cd4a5db2d7384bd1328..2df44877378e1f8703b80b2bfdb4b4ad3b354e43 100644 (file)
--- 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 3caf034a3f82dcbdb1aa4516b2f5716fbe2139c4..8a47418b68009a5b5e09a11d7d7a9c4b8f66cc7e 100644 (file)
--- a/matita/matita/matita.lang
+++ b/matita/matita/matita.lang
@@ -106,6 +106,7 @@
          <keyword>inversion</keyword>
          <keyword>lapply</keyword>
          <keyword>destruct</keyword>
+         <keyword>assume</keyword>
 
           <!-- commands -->
           <keyword>alias</keyword>