Removing "exact" from the tactic AST.

11 files changed, 24 insertions, 19 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 0a0927b3f..e1d480960 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -139,7 +139,6 @@ type intro_pattern_naming = intro_pattern_naming_expr located
 type 'a gen_atomic_tactic_expr =
   (* Basic tactics *)
   | TacIntroPattern of 'dtrm intro_pattern_expr located list
-  | TacExact of 'trm
   | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
       ('nam * 'dtrm intro_pattern_expr located option) option
   | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index efabdc4ad..8e37653f5 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 0bddcc9fd..9a2a176cb 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 4d1d8ba7f..2118e87b1 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 bd48ffb72..c1c7be1cc 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 c8fa9367f..c51c36538 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 8bb6ee4cd..6f64981ef 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 1e974d6f5..3c1a384ce 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) ->
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 993695fb9..6e1731bb2 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -529,8 +529,6 @@ GEXTEND Gram
       | IDENT "intros" ->
           TacAtom (!@loc, TacIntroPattern [!@loc,IntroForthcoming false])
 
-      | IDENT "exact"; c = constr -> TacAtom (!@loc, TacExact c)
-
       | IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ",";
           inhyp = in_hyp_as -> TacAtom (!@loc, TacApply (true,false,cl,inhyp))
       | IDENT "eapply"; cl = LIST1 constr_with_bindings_arg SEP ",";
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index e4d155499..633ff1876 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -827,8 +827,6 @@ module Make
         | TacIntroPattern (_::_ as p) ->
           hov 1 (primitive "intros" ++ spc () ++
                     prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)
-        | TacExact c ->
-          hov 1 (primitive "exact" ++ pr_constrarg c)
         | TacApply (a,ev,cb,inhyp) ->
           hov 1 (
             (if a then mt() else primitive "simple ") ++
diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v
index fc60897d2..fc4c171e2 100644
--- a/test-suite/bugs/closed/3649.v
+++ b/test-suite/bugs/closed/3649.v
@@ -2,6 +2,7 @@
 (* File reduced by coq-bug-finder from original input, then from 9518 lines to 404 lines, then from 410 lines to 208 lines, then from 162 lines to 77 lines *)
 (* coqc version trunk (September 2014) compiled on Sep 18 2014 21:0:5 with OCaml 4.01.0
    coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *)
+Declare ML Module "coretactics".
 Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
 Reserved Notation "x = y" (at level 70, no associativity).
 Delimit Scope type_scope with type.