]> matita.cs.unibo.it Git - helm.git/commit
Universe is used only locally to tactics/
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 16 Apr 2009 09:46:57 +0000 (09:46 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 16 Apr 2009 09:46:57 +0000 (09:46 +0000)
commitb4f6b1a39b59e923527f5c17d8fdd0fa1e13e1bf
tree45a975861d40782f970ea0e0536e8dfe47b1a3bf
parentec0b4acecb86886baf5f785da270fd60e7910b32
Universe is used only locally to tactics/
AutomationCache.cache is part of grafite_status and will
contain tables too
16 files changed:
helm/software/components/binaries/transcript/.depend.opt
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/grafite_engine/grafiteSync.ml
helm/software/components/grafite_engine/grafiteTypes.ml
helm/software/components/grafite_engine/grafiteTypes.mli
helm/software/components/syntax_extensions/.depend
helm/software/components/tactics/.depend
helm/software/components/tactics/Makefile
helm/software/components/tactics/auto.ml
helm/software/components/tactics/auto.mli
helm/software/components/tactics/automationCache.ml [new file with mode: 0644]
helm/software/components/tactics/automationCache.mli [new file with mode: 0644]
helm/software/components/tactics/declarative.ml
helm/software/components/tactics/declarative.mli
helm/software/components/tactics/tactics.mli
helm/software/matita/matitaScript.ml