]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a075b56) | patch
This patch allows generation of minimally dependent discrimination principles
authorWilmer Ricciotti <ricciott@cs.unibo.it>
Fri, 5 Oct 2012 10:08:05 +0000 (10:08 +0000)
committerWilmer Ricciotti <ricciott@cs.unibo.it>
Fri, 5 Oct 2012 10:08:05 +0000 (10:08 +0000)
commit3d981fb10ebc350bc3fc693f0a433d51fc35715a
tree3b74b558f973e310af0e09586b6135b748dca42ftree | snapshot
parenta075b56c257c63d10b85b3f130d2286366ddc165commit | diff
This patch allows generation of minimally dependent discrimination principles
for inductive types, in the case where Leibniz equality is used.
matita/components/grafite_engine/grafiteEngine.ml diff | blob | history
matita/components/ng_tactics/nDestructTac.ml diff | blob | history
matita/components/ng_tactics/nDestructTac.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.