set trace off .

in src/allfiles.maude

mod MSR-MAIN is

protecting MSR-COMMANDS .
protecting MSR-INITIAL-CONTEXT .
protecting MSR-TESTS .

op  init : -> System .

rl  [init] : 
    init => 
    [nil, initialMSRState,
      if allTests :: PassedTests then 
        '\n '*** natToQid(numPassedTests(allTests)) 'tests 'succeeded
	'- 'MSR 'Prototype 'ready '*** '\n
      else
        '\n '*** 'UNIT 'TESTS 'FAILED ': failedTests(allTests)
	'; natToQid(numPassedTests(allTests)) 'passed '*** '\n
      fi] .

endm

--- set trace on .
set trace condition on .
set trace substitution on .
--- set trace whole on .
set print color on .
trace exclude SUBSTITUTION-RULES META-SUBSTITUTION CONSTRAINTS VAR-UTILS ORACLE .

loop init .

***(
--- TEST CASE BEGINS HERE

--- works:
rew ['t:type.,context(emptyCtxt),nil] .
--- works:
red metaRewrite(upModule('MSR-MAIN, false), upTerm( ['t:type.,context(emptyCtxt),nil] ), unbounded).
--- doesn't work:
red metaRewrite(upModule('MSR-COMMANDS, false), upTerm( ['t:type.,context(emptyCtxt),nil] ), unbounded).
)