The Coq mailing list

[Victor Porton <porton AT narod.ru>]

09.01.2013, 15:52, "Victor Porton" 
<porton AT narod.ru>:
> The following is my proposal to add a new feature to Coq:
>
> Add and remove hints to a new kind of hints databases which I call 
> "general" hints:
>
> Create General Hint <db>.
> [Local] General Hint <db>: <term-1>...<term-n>. (* add n terms to the DB *)
> [Local] Remove General Hint <db>.

Sorry, 
Remove General Hint <db>: <term-1>...<term-n>.

> Now for a hint database named "dual_order" it can be used as follows (with 
> $ used to refer to general hints DB):
>
> rewrite $dual_order
>
> would be equivalent to
>
> rewrite <term-1>, ..., <term-n>
>
> (if the DB "dual_order" contains <term-1>, ..., <term-n>)
>
> and maybe likewise in other tactics, I haven't yet considered that in 
> details.
>
> We could also mix references to general hints databases with plain IDs like 
> this:
>
> rewrite $dual_order, my_rule, $dual_category.
>
> My proposal is not perfect. The following are the deficiencies:
>
> 1. I provide no mean to control that all hints inserted in such hints 
> databases are setoid equalities.
>
> 2. There should be a way to pass "references" to general hint databases, 
> that is variables containing a reference to a hint database. This way for 
> example code for both order duality and categorical duality can be shared. 
> The best thing for this I invented for now is double-dollar notation like:
>
> rewrite $$dbref.
>
> I haven't yet realized what database reference should be. Should these be 
> simply strings (with database names)?
>
> Finally, if nobody is willing to implement this, I TREAT you that I will 
> learn ML and do it myself!

Oh, certainly I THREAT not treat. :-)

-- 
Victor Porton - http://portonvictor.org