From 011ac2d7db53f0df2849985ef9cc044574c0ddb0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 13 Apr 2016 16:44:42 +0200
Subject: Switching to an untyped toplevel representation for Ltac values.

---
 engine/geninterp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine')

diff --git a/engine/geninterp.ml b/engine/geninterp.ml
index 0080758000..0d67213674 100644
--- a/engine/geninterp.ml
+++ b/engine/geninterp.ml
@@ -32,4 +32,4 @@ let register_interp0 = Interp.register0
 let generic_interp ist (GenArg (Glbwit wit, v)) =
   let open Ftactic.Notations in
   interp wit ist v >>= fun ans ->
-  Ftactic.return (Val.Dyn (val_tag (topwit wit), ans))
+  Ftactic.return (Val.inject (val_tag (topwit wit)) ans)
-- 
cgit v1.2.3