projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: fbdd1cc) | patch
In some cases (e.g. JM equality) the inversion principle is not generated
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 18 May 2007 13:34:45 +0000 (13:34 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 18 May 2007 13:34:45 +0000 (13:34 +0000)
commitd52416a2c32c74f28ff0ea2f4bc076e6d3ee30f7
tree84220e115045f5fab82bc4cacea2c284088e32b6tree | snapshot
parentfbdd1cc46819d19ed135391a4a954c19d1b92c0ccommit | diff
In some cases (e.g. JM equality) the inversion principle is not generated
because CicRefine cannot infer a dependetly enough type. Now a warning is
raised and compilation is not stopped.
components/tactics/inversion_principle.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.