]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c6cc2a7) | 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)
commit47988107f44566d53fd5a71fd64a015bbf24a380
tree8c5025dc512448341c715c8f783ab4a5f9187aaetree | snapshot
parentc6cc2a7227d6750076f591a62d7b1896ebf1ebfacommit | 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.
helm/software/components/tactics/inversion_principle.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.