Commit c6af90f5 authored by Heiko Becker's avatar Heiko Becker
Browse files

Fix bug in certificate generation

parent b7f792ff
......@@ -512,8 +512,8 @@ object CertificatePhase extends DaisyPhase {
private def hol4AbsEnv (e:Expr, errorMap:Map[Expr, Rational], rangeMap:Map[Expr, Interval], cont:String) :String =
//must be set TODO:Assert?
val nameE = expressionNames(e)
// see coqAbsenv
val nameE = expressionNames.getOrElse(e,"FOO")
e match {
case x @ Variable(id) =>
val intvE = hol4Interval((rangeMap(x).xlo,rangeMap(x).xhi))
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment