]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1c055e6) | patch
Patch applied to the locate query: when used to retrieve the first inductive
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 9 Sep 2002 10:03:24 +0000 (10:03 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 9 Sep 2002 10:03:24 +0000 (10:03 +0000)
commit8d1b8c31da7bdfb695636bd4ef1c7c948ce511c4
tree8e24456f4cd8e1fd5d6ff9c654eb77735271d281tree | snapshot
parent1c055e64e5a1a37112622548e54326c658552de6commit | diff
Patch applied to the locate query: when used to retrieve the first inductive
type of a mutual inductive types block, the returned URI is now the URI of
the type (with the fragment identifier!) and not the one of the block (without).
helm/gTopLevel/mQueryGenerator.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.