]> matita.cs.unibo.it Git - helm.git/commit
Much simpler (and slightly more performant) implementation of the UriManager.
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 23 Jun 2005 17:05:01 +0000 (17:05 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 23 Jun 2005 17:05:01 +0000 (17:05 +0000)
commita458a3e72fd374b106481a7e98f4000369c6ae61
treec357eddbf3f01564525e4fba39d5e640133c32f9
parentfaabe59afc8e66c96a1191210ac1e97effa028fe
Much simpler (and slightly more performant) implementation of the UriManager.
helm/matita/matitaScript.ml
helm/matita/matitaSync.ml
helm/ocaml/metadata/metadataConstraints.ml
helm/ocaml/metadata/metadataExtractor.ml
helm/ocaml/tactics/autoTactic.ml
helm/ocaml/urimanager/uriManager.ml
helm/ocaml/urimanager/uriManager.mli