Using higher-order representation for closures.

1 files changed, 9 insertions, 20 deletions

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;