From 4c964aa3ecfbb2f6aa52274545c2e27d7d11e179 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Aug 2017 16:37:39 +0200
Subject: Fix typing of reference quotations.

---
 src/tac2core.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/tac2core.ml b/src/tac2core.ml
index 196755346d..b38f0b8582 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -21,6 +21,7 @@ open Proofview.Notations
 
 module Value = Tac2ffi
 
+let std_core n = KerName.make2 Tac2env.std_prefix (Label.of_id (Id.of_string_soft n))
 let coq_core n = KerName.make2 Tac2env.coq_prefix (Label.of_id (Id.of_string_soft n))
 
 module Core =
@@ -35,6 +36,7 @@ let t_constr = coq_core "constr"
 let t_pattern = coq_core "pattern"
 let t_ident = coq_core "ident"
 let t_option = coq_core "option"
+let t_reference = std_core "reference"
 
 let c_nil = coq_core "[]"
 let c_cons = coq_core "::"
@@ -730,7 +732,7 @@ let () =
 let () =
   let interp _ gr = return (Value.of_reference gr) in
   let obj = {
-    ml_type = t_pattern;
+    ml_type = t_reference;
     ml_interp = interp;
   } in
   define_ml_object Tac2env.wit_reference obj
-- 
cgit v1.2.3