The Coq mailing list

[Julien Forest <forest AT ensiie.fr>]

Dear Adriaan, 


On Wed, 9 Apr 2008 16:47:50 +0200
Adriaan Moors 
<adriaan.moors AT gmail.com>
 wrote:

> 
> Thank you for the hint about inlining subst_mems! Is it discussed in a  
> FAQ that I should have read?

I'm not sure about that maybe someone else can give you a pointer.

> 
> I implemented your suggestion, and now my fixpoint is accepted, but on  
> using Functional Scheme, I get:
> "Anomaly: add_args : todo. Please report."
>

1- The error message is not the good one ! 
2- Yes. For now, and once again probably for a long time,  such a body cannot 
be accepted. 


> Is this the restriction you mentioned? I guess the only way to use  
> functional induction without defining the (huge) induction principles  
> by hand (which I've already done for the normal induction principles)  
> is to remove nested occurrences of list etc in my datatypes (as  
> illustrated in my example below). That'd be quite unfortunate :-(
> 
> cheers,
> adriaan
> 
Cheers, 
Julien. 
ps: can you send me (by private mail we do not need to polute this list) the 
version of coq you use so that I can correct the error message. 

J.