]> matita.cs.unibo.it Git - helm.git/commit
added choose_uri method to console, used by the interpreter to implement the
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 14 Feb 2005 15:12:24 +0000 (15:12 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 14 Feb 2005 15:12:24 +0000 (15:12 +0000)
commitab336f7c09d052c45a09dd49e9b75a39e8b57e5b
tree65ef566bf0a4b7a333a4cc2661fe6b5cde80f7cd
parenteea144a45e0b58530daeb9a33f79a81a78bd3c9a
added choose_uri method to console, used by the interpreter to implement the
hint command
helm/matita/matitaGui.ml
helm/matita/matitaGui.mli
helm/matita/matitaInterpreter.ml
helm/matita/matitaMisc.ml
helm/matita/matitaTypes.ml
helm/matita/matitaTypes.mli
helm/matita/matitac.ml