]> matita.cs.unibo.it Git - helm.git/commit
New version(s) of hint. One more stable (hint) and one more experimental
authorAndrea Asperti <andrea.asperti@unibo.it>
Thu, 4 Nov 2004 10:22:18 +0000 (10:22 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Thu, 4 Nov 2004 10:22:18 +0000 (10:22 +0000)
commit7065757f75d899ef1751cfc3b30fa523fe903bf8
treea466375e33bc50da9ce3df506087b678655f747f
parent6e986001aac7cc63b0e7d13447caae3729e0f833
New version(s) of hint. One more stable (hint) and one more experimental
experimental_hint. The latter uses apply_verbose, since it needs to
get back the subproof of the goal, usually not returned by tactics.
helm/ocaml/tactics/metadataQuery.ml
helm/ocaml/tactics/metadataQuery.mli