]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4080c4f) | patch
1) GrafiteAst.NEval => GrafiteAst.NReduce
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 18 May 2009 11:59:53 +0000 (11:59 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 18 May 2009 11:59:53 +0000 (11:59 +0000)
commita9c8d96d47a5895c99bca2fe93decf464bca62c3
treef30c74fff35d9e7a86d08b2d10098a291819fc2atree | snapshot
parent4080c4f65aa9f69af505530dfbbe94ffede8052ecommit | diff
1) GrafiteAst.NEval => GrafiteAst.NReduce
2) new tactic "nnormalize" implemented
3) "ngeneralize" now uses "wanted" when no term is selected
   (so that it is possible to use ngeneralize to move an
   hypothesis down)
4) new syntax for non punctuational tinycals was missing
helm/software/components/grafite/grafiteAst.ml diff | blob | history
helm/software/components/grafite_engine/grafiteEngine.ml diff | blob | history
helm/software/components/grafite_parser/grafiteParser.ml diff | blob | history
helm/software/components/ng_tactics/.depend diff | blob | history
helm/software/components/ng_tactics/.depend.opt diff | blob | history
helm/software/components/ng_tactics/nTactics.ml diff | blob | history
helm/software/components/ng_tactics/nTactics.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.