coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: scott constable <sdconsta AT syr.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Definitions for Parsing Compatibility
Date: Wed, 17 Feb 2016 16:51:41 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=sdconsta AT syr.edu; spf=None smtp.mailfrom=sdconsta AT syr.edu; spf=None smtp.helo=postmaster AT smtp1.syr.edu
Ironport-phdr: 9a23:Kcp5wxfV1EGwM7fxqAFgLLKllGMj4u6mDksu8pMizoh2WeGdxc65Yx7h7PlgxGXEQZ/co6odzbGG7Oa8BydZu8jJmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvipNuPPU4R3mT1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu2pN5g/GLdfFXEtN30/zMztrxjKCwWVtVUGVWBDiRFPHxSN5xb8RYv4uC/3/r5m1CKdO9bqRJgvSC7k4qt2Hky7wBwbPiI0pTmEwvd7i7hW9Uqs

Hi All,

I've notice that the Software Foundations book has the following code in LibTactics.v:

(* ---------------------------------------------------------------------- *)

(** ** Definitions for parsing compatibility *)

Tactic Notation "f_equal" :=

f_equal.

Tactic Notation "constructor" :=

constructor.

Tactic Notation "simple" :=

simpl.

Tactic Notation "split" :=

split.

Tactic Notation "right" :=

right.

Tactic Notation "left" :=

left.

(* ---------------------------------------------------------------------- *)

What exactly is the purpose of reintroducing existing tactics as identical notations?

Thanks in advance,

~Scott Constable

[Coq-Club] Definitions for Parsing Compatibility, scott constable, 02/17/2016
- Re: [Coq-Club] Definitions for Parsing Compatibility, Pierre Courtieu, 02/18/2016
- Re: [Coq-Club] Definitions for Parsing Compatibility, Pierre-Marie Pédrot, 02/18/2016
  - Re: [Coq-Club] Definitions for Parsing Compatibility, scott constable, 02/18/2016
    - Re: [Coq-Club] Definitions for Parsing Compatibility, Pierre Courtieu, 02/20/2016
      - Re: [Coq-Club] Definitions for Parsing Compatibility, scott constable, 02/20/2016