Removing "exact" from the tactic AST.

7 files changed, 23 insertions, 14 deletions

diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index efabdc4ad7..8e37653f57 100644
--- a/ltac/coretactics.ml4
+++ b/ltac/coretactics.ml4
@@ -26,6 +26,10 @@ TACTIC EXTEND reflexivity
   [ "reflexivity" ] -> [ Tactics.intros_reflexivity ]
 END
 
+TACTIC EXTEND exact
+  [ "exact" casted_constr(c) ] -> [ Tactics.exact_no_check c ]
+END
+
 TACTIC EXTEND assumption
   [ "assumption" ] -> [ Tactics.assumption ]
 END
diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4
index 0bddcc9fdd..9a2a176cbf 100644
--- a/ltac/extraargs.ml4
+++ b/ltac/extraargs.ml4
@@ -15,6 +15,7 @@ open Constrarg
 open Pcoq.Prim
 open Pcoq.Constr
 open Names
+open Tacmach
 open Tacexpr
 open Taccoerce
 open Tacinterp
@@ -175,6 +176,16 @@ ARGUMENT EXTEND lglob
   [ lconstr(c) ] -> [ c ]
 END
 
+let interp_casted_constr ist gl c =
+  interp_constr_gen (Pretyping.OfType (pf_concl gl)) ist (pf_env gl) (project gl) c
+
+ARGUMENT EXTEND casted_constr
+  TYPED AS constr
+  PRINTED BY pr_gen
+  INTERPRETED BY interp_casted_constr
+  [ constr(c) ] -> [ c ]
+END
+
 type 'id gen_place= ('id * hyp_location_flag,unit) location
 
 type loc_place = Id.t Loc.located gen_place
diff --git a/ltac/extraargs.mli b/ltac/extraargs.mli
index 4d1d8ba7fe..2118e87b11 100644
--- a/ltac/extraargs.mli
+++ b/ltac/extraargs.mli
@@ -38,6 +38,11 @@ val wit_lconstr :
   Tacexpr.glob_constr_and_expr,
   Constr.t) Genarg.genarg_type
 
+val wit_casted_constr :
+  (constr_expr,
+  Tacexpr.glob_constr_and_expr,
+  Constr.t) Genarg.genarg_type
+
 val glob : constr_expr Pcoq.Gram.entry
 val lglob : constr_expr Pcoq.Gram.entry
 
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index bd48ffb723..c1c7be1cc9 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -481,7 +481,6 @@ let rec intern_atomic lf ist x =
   (* Basic tactics *)
   | TacIntroPattern l ->
       TacIntroPattern (List.map (intern_intro_pattern lf ist) l)
-  | TacExact c -> TacExact (intern_constr ist c)
   | TacApply (a,ev,cb,inhyp) ->
       TacApply (a,ev,List.map (intern_constr_with_bindings_arg ist) cb,
                 Option.map (intern_in_hyp_as ist lf) inhyp)
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index c8fa9367f3..c51c36538d 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -684,10 +684,6 @@ let interp_typed_pattern ist env sigma (_,c,_) =
     interp_gen WithoutTypeConstraint ist true pure_open_constr_flags env sigma c in
   pattern_of_constr env sigma c
 
-(* Interprets a constr expression casted by the current goal *)
-let pf_interp_casted_constr ist gl c =
-  interp_constr_gen (OfType (pf_concl gl)) ist (pf_env gl) (project gl) c
-
 (* Interprets a constr expression *)
 let pf_interp_constr ist gl =
   interp_constr ist (pf_env gl) (project gl)
@@ -1644,14 +1640,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
              expected behaviour. *)
           (Tactics.intro_patterns l')) sigma
       end }
-  | TacExact c ->
-      (* spiwack: until the tactic is in the monad *)
-      Proofview.Trace.name_tactic (fun () -> Pp.str"<exact>") begin
-      Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
-        let (sigma, c_interp) = pf_interp_casted_constr ist gl c in
-        Sigma.Unsafe.of_pair (Tactics.exact_no_check c_interp, sigma)
-      end }
-      end
   | TacApply (a,ev,cb,cl) ->
       (* spiwack: until the tactic is in the monad *)
       Proofview.Trace.name_tactic (fun () -> Pp.str"<apply>") begin
diff --git a/ltac/tacinterp.mli b/ltac/tacinterp.mli
index 8bb6ee4cdf..6f64981eff 100644
--- a/ltac/tacinterp.mli
+++ b/ltac/tacinterp.mli
@@ -72,6 +72,9 @@ val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map
 val interp_hyp : interp_sign -> Environ.env -> Evd.evar_map ->
   Id.t Loc.located -> Id.t
 
+val interp_constr_gen : Pretyping.typing_constraint -> interp_sign ->
+  Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Evd.evar_map * constr
+
 val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map ->
  glob_constr_and_expr bindings -> Evd.evar_map * constr bindings
 
diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml
index 1e974d6f5d..3c1a384ceb 100644
--- a/ltac/tacsubst.ml
+++ b/ltac/tacsubst.ml
@@ -137,7 +137,6 @@ let rec subst_match_goal_hyps subst = function
 let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   (* Basic tactics *)
   | TacIntroPattern l -> TacIntroPattern (List.map (subst_intro_pattern subst) l)
-  | TacExact c -> TacExact (subst_glob_constr subst c)
   | TacApply (a,ev,cb,cl) ->
       TacApply (a,ev,List.map (subst_glob_with_bindings_arg subst) cb,cl)
   | TacElim (ev,cb,cbo) ->