Support for Coq Notations

[Aqissiaq]

It would be nice if an Ott grammer like

grammar
G {{ tex \Gamma }} :: G_ ::=
  {{ coq gmap nat nat }}
  {{ coq-universe Type }}

Could generate Notation G := (gmap nat nat) instead of Definition G := (gmap nat nat).

The motivating example is std++'s finite maps, where Notation is much more convenient than Definition.

From stdpp Require Import gmap.

(* with Notation, automation works out of the box *)
Notation context := (gmap nat nat).
Fact insert_lookup_ne_context: forall (C:context) i j x y,
    i <> j -> C !! i = Some x -> <[j:=y]> C !! i = Some x.
  by intros; simplify_map_eq.
Qed.

(* with Definition things are much harder *)
Definition context' := gmap nat nat.
Fact insert_lookup_ne_context': forall (C:context') i j x y,
    i <> j -> C !! i = Some x -> <[j:=y]> C !! i = Some x.
Proof.
  intros.
  Fail now simplify_map_eq.
  (* Tactic failure: Cannot solve this goal. *)
  Fail rewrite lookup_insert_ne.
  (* Found no subterm matching "<[?M5058:=?M5060]> ?M5057 !! ?M5059" in the current goal. *)
  now setoid_rewrite lookup_insert_ne.
Qed.

[palmskog]

Thanks, one approach might be to have a coq-notation hom:

grammar
G {{ tex \Gamma }} :: G_ ::=
  {{ coq-notation (gmap nat nat) }}

or

grammar
G {{ tex \Gamma }} :: G_ ::=
  {{ coq (gmap nat nat) }}
  {{ coq-notation }}

[eapiova]

It would be very nice to have this feature