From 7d496e618f35a17b8432ac3c7205138f03c95fd2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Aug 2017 14:58:46 +0200
Subject: Introducing a quotation for global references.

---
 src/tac2env.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'src/tac2env.ml')

diff --git a/src/tac2env.ml b/src/tac2env.ml
index ac2bd5fc23..65276ec57f 100644
--- a/src/tac2env.ml
+++ b/src/tac2env.ml
@@ -246,7 +246,7 @@ let shortest_qualid_of_projection kn =
 
 type 'a ml_object = {
   ml_type : type_constant;
-  ml_interp : environment -> 'a -> Geninterp.Val.t Proofview.tactic;
+  ml_interp : environment -> 'a -> valexpr Proofview.tactic;
 }
 
 module MLTypeObj =
@@ -271,8 +271,9 @@ let std_prefix =
 
 (** Generic arguments *)
 
-let wit_ltac2 = Genarg.make0 "ltac2"
+let wit_ltac2 = Genarg.make0 "ltac2:value"
 let wit_pattern = Genarg.make0 "ltac2:pattern"
+let wit_reference = Genarg.make0 "ltac2:reference"
 
 let is_constructor qid =
   let (_, id) = repr_qualid qid in
-- 
cgit v1.2.3