The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

I'm having a strange issue with the simpl tactic.

I have a function (Say f) defined using the Fixpoint keyword.

When f is defined outside any section, simpl happily reduces

f whenever the  structure of its recursive argument is known.

As soon as I move f into a section

where some of its arguments 

become section variables, simpl stops reducing f in

*other* sections even

when the  structure of its recursive argument is known.

I can unfold f, and then successfully do simpl. However, that leaves a 

large fix _expression_ after the reduction step.

I cannot reproduce this problem on a small enough example.

In all of the toy examples I tried to write, simpl works just fine.

 

Does someone know what could be going wrong?

I can share the source files required to reproduce the issue

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/