diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-02-27 11:02:55 +0100 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-02-27 11:02:55 +0100 |
| commit | 35a0c9b1f7fab940affe676f8b8c5cdd36071172 (patch) | |
| tree | eecd8d317f847e0abc3dc7661ec304edfa0a48c5 | |
| parent | 26134d1c4056b70b2bdadaf881ef951e5858b606 (diff) | |
Tacinterp: spurious enterl.
This changes the tacinterp API, but only affects (one line of) the MapleMode contrib.
| -rw-r--r-- | tactics/tacinterp.ml | 6 | ||||
| -rw-r--r-- | tactics/tacinterp.mli | 4 |
2 files changed, 2 insertions, 8 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index ad0ec0b59..3e4394228 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 79b7f6fd5..0c89eb3a2 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 |