From 714a72985d3123bf2ef3e8c67cdcefc23990ab53 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 31 Oct 2017 16:45:47 +0100
Subject: Do not identify a pre_ident as a string Ltac value.

It should be printed without quotes and it already has its
interpretation function.
---
 interp/stdarg.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/stdarg.ml')

diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 45dec5112b..65c55a584a 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -28,7 +28,7 @@ let wit_string : string uniform_genarg_type =
   make0 "string"
 
 let wit_pre_ident : string uniform_genarg_type =
-  make0 ~dyn:(val_tag (topwit wit_string)) "preident"
+  make0 "preident"
 
 let loc_of_or_by_notation f = function
   | AN c -> f c
-- 
cgit v1.2.3