7 files changed, 67 insertions, 2 deletions
diff --git a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
index adabb7a0a0..8447cf10db 100644
--- a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
+++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
@@ -11,7 +11,7 @@ let evil t f =
   let te = Declare.definition_entry
       ~univs:(Monomorphic_entry (ContextSet.singleton u)) tu
   in
-  let tc = Declare.declare_constant t (DefinitionEntry te, k) in
+  let tc = Declare.declare_constant t (Declare.DefinitionEntry te, k) in
   let tc = mkConst tc in
 
   let fe = Declare.definition_entry
@@ -19,4 +19,4 @@ let evil t f =
       ~types:(Term.mkArrowR tc tu)
       (mkLambda (Context.nameR (Id.of_string "x"), tc, mkRel 1))
   in
-  ignore (Declare.declare_constant f (DefinitionEntry fe, k))
+  ignore (Declare.declare_constant f (Declare.DefinitionEntry fe, k))
diff --git a/test-suite/misc/quotation_token.sh b/test-suite/misc/quotation_token.sh
new file mode 100755
index 0000000000..6357e8d7ce
--- /dev/null
+++ b/test-suite/misc/quotation_token.sh
@@ -0,0 +1,31 @@
+#!/usr/bin/env bash
+
+set -e
+
+export COQBIN=$BIN
+export PATH=$COQBIN:$PATH
+
+cd misc/quotation_token/
+
+coq_makefile -f _CoqProject -o Makefile
+
+make clean
+
+make src/quotation_plugin.cma
+
+TMP=`mktemp`
+
+if make > $TMP 2>&1; then
+  echo "should fail"
+  rm $TMP
+  exit 1
+fi
+
+if grep "File.*quotation.v., line 12, characters 6-30" $TMP; then
+  rm $TMP
+  exit 0
+else
+  echo "wong loc: `grep File.*quotation.v $TMP`"
+  rm $TMP
+  exit 1
+fi
diff --git a/test-suite/misc/quotation_token/.gitignore b/test-suite/misc/quotation_token/.gitignore
new file mode 100644
index 0000000000..18da256f3e
--- /dev/null
+++ b/test-suite/misc/quotation_token/.gitignore
@@ -0,0 +1,2 @@
+/Makefile*
+/src/quotation.ml
diff --git a/test-suite/misc/quotation_token/_CoqProject b/test-suite/misc/quotation_token/_CoqProject
new file mode 100644
index 0000000000..1b3e7c6399
--- /dev/null
+++ b/test-suite/misc/quotation_token/_CoqProject
@@ -0,0 +1,6 @@
+-Q theories Quotation
+-I src
+
+src/quotation.mlg
+src/quotation_plugin.mlpack
+theories/quotation.v
diff --git a/test-suite/misc/quotation_token/src/quotation.mlg b/test-suite/misc/quotation_token/src/quotation.mlg
new file mode 100644
index 0000000000..961b170a0d
--- /dev/null
+++ b/test-suite/misc/quotation_token/src/quotation.mlg
@@ -0,0 +1,12 @@
+{
+open Pcoq.Constr
+}
+GRAMMAR EXTEND Gram
+  GLOBAL: operconstr;
+
+  operconstr: LEVEL "0"
+    [ [ s = QUOTATION "foobar:" ->
+        {
+          CAst.make ~loc Constrexpr.(CSort Glob_term.(UNamed [GProp,0])) } ] ]
+  ;
+END
diff --git a/test-suite/misc/quotation_token/src/quotation_plugin.mlpack b/test-suite/misc/quotation_token/src/quotation_plugin.mlpack
new file mode 100644
index 0000000000..b372b94b30
--- /dev/null
+++ b/test-suite/misc/quotation_token/src/quotation_plugin.mlpack
@@ -0,0 +1 @@
+Quotation
diff --git a/test-suite/misc/quotation_token/theories/quotation.v b/test-suite/misc/quotation_token/theories/quotation.v
new file mode 100644
index 0000000000..66326e89c1
--- /dev/null
+++ b/test-suite/misc/quotation_token/theories/quotation.v
@@ -0,0 +1,13 @@
+
+Declare ML Module "quotation_plugin".
+
+Definition x := foobar:{{ hello
+  there
+}}.
+
+Definition y := foobar:{{ another
+  multi line
+  thing
+}}.
+Check foobar:{{ oops
+ ips }} y.