diff --git a/template-coq/src/constr_denoter.ml b/template-coq/src/constr_denoter.ml index 56f5395d2..98945be9f 100644 --- a/template-coq/src/constr_denoter.ml +++ b/template-coq/src/constr_denoter.ml @@ -93,9 +93,9 @@ struct let unquote_string trm = let rec go n trm = let (h,args) = app_full trm [] in - if constr_equall h tEmptyString then + if constr_equall h tBsEmptyString then Bytes.create n - else if constr_equall h tString then + else if constr_equall h tBsString then match args with c :: s :: [] -> let res = go (n + 1) s in diff --git a/template-coq/src/constr_quoter.ml b/template-coq/src/constr_quoter.ml index fff2a8d20..aab8d1d31 100644 --- a/template-coq/src/constr_quoter.ml +++ b/template-coq/src/constr_quoter.ml @@ -156,10 +156,10 @@ struct let rec go from acc = if from < 0 then acc else - let term = constr_mkApp (tString, [| quote_char (String.get s from) ; acc |]) in + let term = constr_mkApp (tBsString, [| quote_char (String.get s from) ; acc |]) in go (from - 1) term in - go (len - 1) (Lazy.force tEmptyString) + go (len - 1) (Lazy.force tBsEmptyString) let quote_string s = try Hashtbl.find string_hash s diff --git a/template-coq/src/constr_reification.ml b/template-coq/src/constr_reification.ml index c590bb610..d56ead567 100644 --- a/template-coq/src/constr_reification.ml +++ b/template-coq/src/constr_reification.ml @@ -67,8 +67,8 @@ struct let template s = resolve ("metacoq.template." ^ s) let template_ref s = resolve_ref ("metacoq.template." ^ s) - let tString = resolve "metacoq.string.cons" - let tEmptyString = resolve "metacoq.string.nil" + let tBsString = resolve "metacoq.string.cons" + let tBsEmptyString = resolve "metacoq.string.nil" let tO = resolve "metacoq.nat.zero" let tS = resolve "metacoq.nat.succ" let tnat = resolve "metacoq.nat.type" @@ -151,12 +151,12 @@ struct let tmk_branch = ast "mk_branch" let tmkdecl = ast "mkdecl" let (tTerm,tRel,tVar,tEvar,tSort,tCast,tProd, - tLambda,tLetIn,tApp,tCase,tFix,tConstructor,tConst,tInd,tCoFix,tProj,tInt,tFloat,tArray) = + tLambda,tLetIn,tApp,tCase,tFix,tConstructor,tConst,tInd,tCoFix,tProj,tInt,tFloat,tString,tArray) = (ast "term", ast "tRel", ast "tVar", ast "tEvar", ast "tSort", ast "tCast", ast "tProd", ast "tLambda", ast "tLetIn", ast "tApp", ast "tCase", ast "tFix", ast "tConstruct", ast "tConst", ast "tInd", ast "tCoFix", ast "tProj", ast "tInt", ast "tFloat", - ast "tArray") + ast "tString", ast "tArray") let tkername = ast "kername" let tmodpath = ast "modpath" let tMPfile = ast "MPfile" diff --git a/template-coq/theories/Constants.v b/template-coq/theories/Constants.v index a8ea5dd3e..d1098f4a3 100644 --- a/template-coq/theories/Constants.v +++ b/template-coq/theories/Constants.v @@ -178,6 +178,7 @@ Register MetaCoq.Template.Ast.tFix as metacoq.ast.tFix. Register MetaCoq.Template.Ast.tCoFix as metacoq.ast.tCoFix. Register MetaCoq.Template.Ast.tInt as metacoq.ast.tInt. Register MetaCoq.Template.Ast.tFloat as metacoq.ast.tFloat. +Register MetaCoq.Template.Ast.tString as metacoq.ast.tString. Register MetaCoq.Template.Ast.tArray as metacoq.ast.tArray. (* Local and global declarations *) diff --git a/test-suite/bug_quote_pstring.v b/test-suite/bug_quote_pstring.v new file mode 100644 index 000000000..2142d4d2d --- /dev/null +++ b/test-suite/bug_quote_pstring.v @@ -0,0 +1,8 @@ +(* See PR #1109. *) + +From MetaCoq.Template Require Import All. +From Coq Require Import PrimString. + +MetaCoq Quote Definition quote_test := "quote_me"%pstring. +MetaCoq Unquote Definition unquote_test := (tString "unquote_me"%pstring). +