coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] "simpl" question

From: Marcus Ramos <marcus.ramos AT univasf.edu.br>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] "simpl" question
Date: Thu, 8 May 2014 17:05:05 +0200

Dear All,

When I use the "simpl" tactic in a goal, it changes a subterm of the form "c ++ s", with c: ascii and s: string, into "String c s" (String is a constructor of the type string). How can I prevent simpl from doing this?

Thanks in advance,

Marcus.

[Coq-Club] "simpl" question, Marcus Ramos, 05/08/2014
- Re: [Coq-Club] "simpl" question, Jonathan, 05/09/2014
  - Re: [Coq-Club] "simpl" question, Marcus Ramos, 05/09/2014
    - Re: [Coq-Club] "simpl" question, Kirill Taran, 05/09/2014
      - Re: [Coq-Club] "simpl" question, Marcus Ramos, 05/10/2014
- Re: [Coq-Club] "simpl" question, CJ Bell, 05/09/2014