]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 468e3b3) | patch
Elim generalized: the term to eliminate is now saturated (i.e. it is applied
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 8 Jul 2005 12:15:48 +0000 (12:15 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 8 Jul 2005 12:15:48 +0000 (12:15 +0000)
commite6005301fcbccbca31571795ed6071283f45d5a8
treec32ad14d832bd8491e50302362144336601541adtree | snapshot
parent468e3b35a467e49edb8e5e83469d24520aff83eecommit | diff
Elim generalized: the term to eliminate is now saturated (i.e. it is applied
to as many ? as needed to make its type become something different from a
product).
helm/ocaml/tactics/primitiveTactics.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.