coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Definitions for Parsing Compatibility

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Definitions for Parsing Compatibility
Date: Thu, 18 Feb 2016 10:27:11 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f41.google.com
Ironport-phdr: 9a23:aPwOchThs9pca+9g/Y1fkyB9gNpsv+yvbD5Q0YIujvd0So/mwa64Yx2N2/xhgRfzUJnB7Loc0qyN4/+mBTNLuMzQ+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8KVP1oD3WDsKZpJbzyI7izp/vEMhoVjLqtjgjDomVBvP9ps+GVzOFiIlAz97MrjtLRq8iBXpu5zv5UYCfayV+0CQLdZFDUrNXwurI2u7EGbDFjH2nxJeWIP2jFMHgKNuBr9R9L6tjbwnut7wiiTe8PsG+MaQzOnup9qRQXyhW8sMCMj7GDal4QklKNWugis4Rd43pTIYYyIHPV7d6LZO9gdQDwSDY5qSyVdD9bkPMM0BO0bMLMd9tGlqg==

I think tactics defined in ocaml are sometimes not registered as Ltac
tactics and thus cannot be use as arguments of other tactics. IMHO
this is a bug and this Tactic Notations are a workaround.

P.

2016-02-17 22:51 GMT+01:00 scott constable
<sdconsta AT syr.edu>:
> 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