[Agda] termination check

[Martin Escardo]

Hello.

I had a big agda file with one function that doesn't temination-checks 
(and that's the way things should be). But apart from this check 
everything went ok, as expected. Now I decided to split this into 
several modules, and I get a problem: when I compile (from emacs) module 
B which uses A, the compilation complains that A doesn't termination 
check and stops. The compilation of A is fine, apart from the 
termination checking. How should I proceed to be able to compile B 
(i.e., how do I make agda "trust me" on this one?)

Thanks.