Skip to content

Conversation

@MathisBD
Copy link
Collaborator

@MathisBD MathisBD commented Oct 29, 2024

This PR fixes the following bug related to quoting primitive strings :

From MetaCoq.Template Require Import All.
From Coq Require Import PrimString.
MetaCoq Test Quote "hello"%pstring.
(* produces (String.String "hello"%pstring) which is ill-typed. *)

The bug comes from the fact that in template-coq's quoting/unquoting code, the ocaml variable named tString is used to refer to two distinct Coq terms :

  • the second constructor of bytestring.string.
  • the primitive string constructor of term.

The fix involves changing the names of a couple ocaml variables : see the diff for more info.

@yforster
Copy link
Member

Could you add a file in the test-suite which checks this behavior? I.e. add the code snippet from the PR as file there?

@yforster
Copy link
Member

Thanks! Once CI goes green I'll squash and merge and cherry-pick the commit over to coq-8.20.

@yforster yforster merged commit 65aa111 into MetaRocq:main Oct 30, 2024
5 checks passed
yforster pushed a commit to yforster/template-coq that referenced this pull request Oct 30, 2024
@MathisBD MathisBD deleted the fix-quote-pstring branch October 30, 2024 14:35
yforster added a commit that referenced this pull request Oct 30, 2024
* initial fix

* update test-suite

Co-authored-by: MathisBD <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants