]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: eac90cc) | patch
Patch to avoid equations of the form ? -> T (oriented this way) that
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 1 Apr 2011 12:43:29 +0000 (12:43 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 1 Apr 2011 12:43:29 +0000 (12:43 +0000)
commitf1c3f85a4e5acf2b6ee52b16103cbb95322016ac
treebeaa306269233e869007fd064f333321830d2e97tree | snapshot
parenteac90ccb93a94f03df9ba5ad853cbd5d8c60b4f2commit | diff
Patch to avoid equations of the form ? -> T (oriented this way) that
can always be applied to later yield non well typed terms.

Moreover, when T is a Leaf and when the goal contains a Leaf, the equation
above is applied breaking one of the "assert (subst=[])" in the code
(since the Leaf is matched by ?).
matita/components/ng_paramodulation/superposition.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.