The Coq mailing list

[Francois Pottier <Francois.Pottier AT inria.fr>]

Hello,

On Sun, Feb 26, 2012 at 11:21:44AM +0100, Pierre Boutillier wrote:
> First of all, if you are only interrested by "simpl" behavior and
> ready to use v8.4, more than Opaque and Transparent that change the
> logical contents of things, you should have a look at Enrico Tassi
> great work about simpl customization :

Thanks, I didn't know about this. It sounds interesting.

> If we reduce the problem to "I would be able to write : opaque bar in simpl"
> then I would suggest to implement "simpl * but bar"

OK, but one would need to clarify whether this means "*in the original goal*,
do not simplify terms whose head variable is bar" or "*in the original goal
and in the subsequent goals that appear after simplification*, do not simplify
terms whose head variable is bar". What I am trying to emulate using Opaque
is the latter behavior.

> Have you in mind "unfold foo; simpl" when you talk about
> "transparent foo in simpl" ?

No, I mentioned "transparent foo in t" just by symmetry with "opaque foo in 
t",
but I don't have a specific use in mind.

I agree that offering more precise ways to control "simpl" is probably a
better route to follow than hacking with opacity and transparency.

-- 
François Pottier
Francois.Pottier AT inria.fr
http://gallium.inria.fr/~fpottier/