clear non-existing assumptions error message Not_found

abella-prover / abella

An interactive theorem prover based on lambda-tree syntax

https://abella-prover.org/

GNU General Public License v3.0

89 stars 18 forks source link

clear non-existing assumptions error message Not_found #73

Closed kyagrd closed 7 years ago

kyagrd commented 7 years ago

Welcome to Abella 2.0.5-dev
Abella < Theorem ff : false.

============================
 false

ff < clear IH H1.
Error: Not_found

 Sorry for displaying a naked OCaml exception. An informative error message
 has not been designed for this situation.

 To help improve Abella's error messages, please file a bug report at
 <https://github.com/abella-prover/abella/issues>. Thanks!

============================
 false