aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorbertot2002-01-23 14:17:57 +0000
committerbertot2002-01-23 14:17:57 +0000
commitbef4e9e5842527ffc76c0ae9635a2188fd09602a (patch)
tree688ef63f0f2bf4f9eee216be7e955c6d27e78d53 /kernel
parent58c4a23cc2d7b01bbc6a7e60d6d074bb0a0e5b26 (diff)
In Pcoq, the search commands had an erroneous behavior. Bound variables
in theorems were renamed to avoid the names present in the current goal's context. This version corrects this problem. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2425 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions