]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c4ea5fd) | patch
1) new tactic normalize (low-level function implemented in
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 18 May 2009 11:57:50 +0000 (11:57 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 18 May 2009 11:57:50 +0000 (11:57 +0000)
commit4080c4f65aa9f69af505530dfbbe94ffede8052e
treeab19629402c871ce8b2c1f7b1a8a28060dbaa58dtree | snapshot
parentc4ea5fdf898b6bbeff10e44046620e8b5bdefbb7commit | diff
1) new tactic normalize (low-level function implemented in
   nCicTacReduction)
2) the select tactic used to generate fresh metavariables by unifying the
   "wanted" part of the pattern in a root where "wanted" did not occur.
   Those metavariables are now removed in that case
helm/software/components/ng_tactics/Makefile diff | blob | history
helm/software/components/ng_tactics/nCicTacReduction.ml [new file with mode: 0644] blob
helm/software/components/ng_tactics/nCicTacReduction.mli [new file with mode: 0644] blob
helm/software/components/ng_tactics/nTacStatus.ml diff | blob | history
helm/software/components/ng_tactics/nTacStatus.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.