diff --git a/modeq/ceval.rml b/modeq/ceval.rml index 48f2885ed1a..b7acceccef2 100644 --- a/modeq/ceval.rml +++ b/modeq/ceval.rml @@ -927,11 +927,11 @@ relation ceval_interactive_functions: (Env.Env, Exp.Exp, Interactive.Interactive => (Values.BOOL(true),st) rule System.time => t1 & - ceval(env,exp,true,SOME(st),NONE) => (value,st') & + ceval(env,exp,true,SOME(st),NONE) => (value,SOME(st')) & System.time => t2 & real_sub(t2,t1) => time ------------------------- - ceval_interactive_functions (env, Exp.CALL(Absyn.IDENT("timing"),[exp],_,_),st as Interactive.SYMBOLTABLE(p,sp,ic,iv,cf)) => (Values.REAL(time),st) + ceval_interactive_functions (env, Exp.CALL(Absyn.IDENT("timing"),[exp],_,_),st) => (Values.REAL(time),st') rule System.set_c_compiler(str) -------------------------