]> matita.cs.unibo.it Git - helm.git/commit
clear now fails if the hypothesys doesnt exist, and doesn not typecheck
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 6 Jul 2005 13:09:16 +0000 (13:09 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 6 Jul 2005 13:09:16 +0000 (13:09 +0000)
commitc56a4b2bad2b1332bc2eda646c18ac547c4ce102
treea6f19574bfa88041457b871683747a4591a404ec
parent2220ec0d80a2846eee56922c76468ad0839f6228
clear now fails if the hypothesys doesnt exist, and doesn not typecheck
the whole context
helm/ocaml/tactics/proofEngineStructuralRules.ml