]> matita.cs.unibo.it Git - helm.git/commit
nauto:
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 21 Oct 2009 13:37:34 +0000 (13:37 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 21 Oct 2009 13:37:34 +0000 (13:37 +0000)
commit1e16d80cc7bf9b73cf5526934b17e2ba955a522a
tree7f111582ce21aa13c6c1b9b116271f9acecdbe19
parentd5aca0dbfdc1770b3fa7e3c1338bfb7ffde8f89e
nauto:
- fixed indexing (now always dome in the same way)
- depth=x means: tray at depth=2 ... try at depth=x
- run auto on set of goals that are linked by occurring in each others types,
  simply distribute if there is no dependency
helm/software/components/ng_tactics/nAuto.ml
helm/software/components/ng_tactics/nTacStatus.ml
helm/software/components/ng_tactics/nTacStatus.mli
helm/software/matita/nlibrary/topology/cantor.ma
helm/software/matita/nlibrary/topology/igft.ma