Commit 5c07cdb7 authored by Heiko Becker's avatar Heiko Becker
Browse files

Fix Bug that would reprdocue already defined variables

parent ed34d15e
......@@ -153,22 +153,20 @@ object CertificatePhase extends DaisyPhase {
private def getValues(e: Expr,reporter:Reporter,prv:String): (String, String) = e match {
case x @ Variable(id) =>
val varId =
if (identifierNums.contains(id))
identifierNums(id)
else{
val tmp = nextFreshVariable()
identifierNums += (id -> tmp)
tmp
}
val (definition,name) =
if (prv == "coq")
coqVariable (id,varId,reporter)
else
holVariable (id,varId,reporter)
expressionNames += (e -> name)
(definition,name)
if (identifierNums.contains(id)){
("",expressionNames(e))
}else{
val varId = nextFreshVariable()
identifierNums += (id -> varId)
val (definition, name) =
if (prv == "coq"){
coqVariable (id,varId,reporter)
}else{
holVariable (id,varId,reporter)
}
expressionNames += (e -> name)
(definition,name)
}
case x @ RealLiteral(r) =>
val (definition, name) =
......
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