The Coq mailing list

[Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>]

Hi

On Mon, Oct 12, 2015 at 12:11:47PM -0400, Jason Gross wrote:
> As suggested in the bug report, you can try something like:
> 
> Tactic Notation "transparent" "assert" "(" ident(H) ":" uconstr(type) ")" :=
>   refine (let H := (_ : type) in _).

This is cool, but there is still a little detail. I take an example
in my code. It was initially
    assert (Saxy : (a = x) * (a = y) → isSet (x = y)).

But, if I add "transparent"
    transparent assert (Saxy : (a = x) * (a = y) → isSet (x = y)).

The "*" is highlighted and I get the message
    Toplevel input, characters 35-36:
    Syntax error: ')' expected after [tactic:uconstr] (in
       [tactic:simple_tactic]).

Same error message if I define "transparent assert" with "constr" or
with "open_constr" instead of "uconstr".

To make it work, I must put the type between parentheses
    transparent assert (Saxy : ((a = x) * (a = y) → isSet (x = y))).

In the simple assert version these parentheses are not required.

-- 
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/