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/tac2interp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/tac2interp.ml')

diff --git a/src/tac2interp.ml b/src/tac2interp.ml
index 664b7de3d6..d3bc79957b 100644
--- a/src/tac2interp.ml
+++ b/src/tac2interp.ml
@@ -105,7 +105,7 @@ let rec interp ist = function
 | GTacExt e ->
   let GenArg (Glbwit tag, e) = e in
   let tpe = Tac2env.interp_ml_object tag in
-  tpe.Tac2env.ml_interp ist e >>= fun e -> return (ValExt e)
+  tpe.Tac2env.ml_interp ist e
 
 and interp_app f args = match f with
 | ValCls { clos_env = ist; clos_var = ids; clos_exp = e } ->
-- 
cgit v1.2.3