From 64a6ac3759b5d0ea635ff284606541b05c696996 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 6 Sep 2017 22:47:44 +0200
Subject: Using higher-order representation for closures.

---
 src/tac2expr.mli | 29 +++++++++--------------------
 1 file changed, 9 insertions(+), 20 deletions(-)

(limited to 'src/tac2expr.mli')

diff --git a/src/tac2expr.mli b/src/tac2expr.mli
index 36c3fbbe59..1b4a704b11 100644
--- a/src/tac2expr.mli
+++ b/src/tac2expr.mli
@@ -180,6 +180,13 @@ type strexpr =
 
 type tag = int
 
+type frame =
+| FrLtac of ltac_constant option
+| FrPrim of ml_tactic_name
+| FrExtn : ('a, 'b) Tac2dyn.Arg.tag * 'b -> frame
+
+type backtrace = frame list
+
 type valexpr =
 | ValInt of int
   (** Immediate integers *)
@@ -187,32 +194,14 @@ type valexpr =
   (** Structured blocks *)
 | ValStr of Bytes.t
   (** Strings *)
-| ValCls of closure
+| ValCls of ml_tactic
   (** Closures *)
 | ValOpn of KerName.t * valexpr array
   (** Open constructors *)
 | ValExt : 'a Tac2dyn.Val.tag * 'a -> valexpr
   (** Arbitrary data *)
 
-and closure = {
-  mutable clos_env : valexpr Id.Map.t;
-  (** Mutable so that we can implement recursive functions imperatively *)
-  clos_var : Name.t list;
-  (** Bound variables *)
-  clos_exp : glb_tacexpr;
-  (** Body *)
-  clos_ref : ltac_constant option;
-  (** Global constant from which the closure originates *)
-}
-
-type frame =
-| FrLtac of ltac_constant option
-| FrPrim of ml_tactic_name
-| FrExtn : ('a, 'b) Tac2dyn.Arg.tag * 'b -> frame
-
-type backtrace = frame list
-
-type ml_tactic = backtrace -> valexpr list -> valexpr Proofview.tactic
+and ml_tactic = backtrace -> valexpr list -> valexpr Proofview.tactic
 
 type environment = {
   env_ist : valexpr Id.Map.t;
-- 
cgit v1.2.3