From 35a0c9b1f7fab940affe676f8b8c5cdd36071172 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 27 Feb 2014 11:02:55 +0100
Subject: Tacinterp: spurious enterl.

This changes the tacinterp API, but only affects (one line of) the MapleMode contrib.---
 tactics/tacinterp.ml  | 6 ------
 tactics/tacinterp.mli | 4 ++--
 2 files changed, 2 insertions(+), 8 deletions(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index ad0ec0b59d..3e43942283 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2175,12 +2175,6 @@ let interp_redexp env sigma r =
   let gist = { fully_empty_glob_sign with genv = env; } in
   interp_red_expr ist sigma env (intern_red_expr gist r)
 
-let val_interp ist (tac:glob_tactic_expr) : typed_generic_argument Proofview.glist Proofview.tactic =
-  Proofview.Goal.enterl (fun gl -> val_interp ist tac gl >= Proofview.Goal.return)
-
-let interp_ltac_constr ist e =
-  Proofview.Goal.enterl (fun gl -> interp_ltac_constr ist e gl >= Proofview.Goal.return)
-
 (***************************************************************************)
 (* Embed tactics in raw or glob tactic expr *)
 
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 79b7f6fd52..0c89eb3a28 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -71,10 +71,10 @@ val interp_genarg : interp_sign -> Environ.env -> Evd.evar_map -> Term.constr ->
   glob_generic_argument -> Evd.evar_map * typed_generic_argument
 
 (** Interprets any expression *)
-val val_interp : interp_sign -> glob_tactic_expr -> value Proofview.glist Proofview.tactic
+val val_interp : interp_sign -> glob_tactic_expr -> Proofview.Goal.t -> value Proofview.tactic
 
 (** Interprets an expression that evaluates to a constr *)
-val interp_ltac_constr : interp_sign -> glob_tactic_expr -> constr Proofview.glist Proofview.tactic
+val interp_ltac_constr : interp_sign -> glob_tactic_expr -> Proofview.Goal.t -> constr Proofview.tactic
 
 (** Interprets redexp arguments *)
 val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map * red_expr
-- 
cgit v1.2.3