]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d5aca0d) | patch
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
tree7f111582ce21aa13c6c1b9b116271f9acecdbe19tree | snapshot
parentd5aca0dbfdc1770b3fa7e3c1338bfb7ffde8f89ecommit | diff
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 diff | blob | history
helm/software/components/ng_tactics/nTacStatus.ml diff | blob | history
helm/software/components/ng_tactics/nTacStatus.mli diff | blob | history
helm/software/matita/nlibrary/topology/cantor.ma diff | blob | history
helm/software/matita/nlibrary/topology/igft.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.