]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6ca487d) | patch
case tactic first tries with a simple outtype and then with a more sofisticated one
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 3 Feb 2009 20:39:00 +0000 (20:39 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 3 Feb 2009 20:39:00 +0000 (20:39 +0000)
commitcf25aeb5fa2c00ebfe93454fbe33421d590506d4
treed9f5e6e96ecd1bb7cf265cdf4d10e2fc25a778f1tree | snapshot
parent6ca487df4f361fd6b0a3b0734396bc6a62b520c3commit | diff
case tactic first tries with a simple outtype and then with a more sofisticated one
only if necessary since refine time may be long
helm/software/components/tactics/primitiveTactics.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.