]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: fbd8a3f) | patch
Bug fixing: the call to MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format'
authorAndrea Asperti <andrea.asperti@unibo.it>
Wed, 1 Sep 2004 07:24:22 +0000 (07:24 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Wed, 1 Sep 2004 07:24:22 +0000 (07:24 +0000)
commit584455a9f581cd2f0fa76a6720c5749b083db8bf
treeac20ca9521c14bd843e9d6720bda190c493c524ctree | snapshot
parentfbd8a3f2e73a821b68172220fad48fd803abbf6ccommit | diff
Bug fixing: the call to MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format'
must be done after filter_new_constants (that compares uris).
helm/ocaml/tactics/tacticChaser.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.