Generalizing the uses of tactic scopes everywhere.

This feature allows the user to write "let x := open_constr(foo) in ..." for instance
without having to resort to tactic notations. Some changes have been introduced in
the parsing of ad-hoc argument scopes, e.g. one has to put parentheses around
constr:(...) and ltac:(...) in tactics. This breaks badly written scripts, although
it is easy to be forward-compatible by preemptively putting thoses parentheses.

5 files changed, 22 insertions, 8 deletions

diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 74d98176a4..7da6df717e 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -19,6 +19,8 @@ open Sigma.Notations
 
 DECLARE PLUGIN "coretactics"
 
+(** Basic tactics *)
+
 TACTIC EXTEND reflexivity
   [ "reflexivity" ] -> [ Tactics.intros_reflexivity ]
 END
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 8f336cdb30..98868e8f91 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -17,6 +17,25 @@ open Tacinterp
 open Misctypes
 open Locus
 
+(** Adding scopes for generic arguments not defined through ARGUMENT EXTEND *)
+
+let create_generic_quotation name e wit =
+  let inject (loc, v) = Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit wit) v) in
+  Egramcoq.create_ltac_quotation name inject (e, None)
+
+let () = create_generic_quotation "integer" Pcoq.Prim.integer Stdarg.wit_int
+let () = create_generic_quotation "string" Pcoq.Prim.string Stdarg.wit_string
+
+let () = create_generic_quotation "ident" Pcoq.Prim.ident Constrarg.wit_ident
+let () = create_generic_quotation "reference" Pcoq.Prim.reference Constrarg.wit_ref
+let () = create_generic_quotation "uconstr" Pcoq.Constr.lconstr Constrarg.wit_uconstr
+let () = create_generic_quotation "constr" Pcoq.Constr.lconstr Constrarg.wit_constr
+let () = create_generic_quotation "ipattern" Pcoq.Tactic.simple_intropattern Constrarg.wit_intro_pattern
+let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Constrarg.wit_open_constr
+let () =
+  let inject (loc, v) = Tacexpr.Tacexp v in
+  Egramcoq.create_ltac_quotation "ltac" inject (Pcoq.Tactic.tactic_expr, Some 5)
+
 (* Rewriting orientation *)
 
 let _ = Metasyntax.add_token_obj "<-"
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index a069fd7557..89dc843cb8 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -651,7 +651,7 @@ and intern_tactic_as_arg loc onlytac ist a =
   | TacCall _ | Reference _
   | TacGeneric _ as a -> TacArg (loc,a)
   | Tacexp a -> a
-  | ConstrMayEval _ | UConstr _ | TacFreshId _ | TacPretype _ | TacNumgoals as a ->
+  | ConstrMayEval _ | TacFreshId _ | TacPretype _ | TacNumgoals as a ->
       if onlytac then error_tactic_expected loc else TacArg (loc,a)
 
 and intern_tactic_or_tacarg ist = intern_tactic false ist
@@ -665,7 +665,6 @@ and intern_tactic_fun ist (var,body) =
 and intern_tacarg strict onlytac ist = function
   | Reference r -> intern_non_tactic_reference strict ist r
   | ConstrMayEval c -> ConstrMayEval (intern_constr_may_eval ist c)
-  | UConstr c -> UConstr (intern_constr ist c)
   | TacCall (loc,f,[]) -> intern_isolated_tactic_reference strict ist f
   | TacCall (loc,f,l) ->
       TacCall (loc,
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 1a8a95158a..bf5f9ddc86 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1365,11 +1365,6 @@ and interp_tacarg ist arg : Val.t Ftactic.t =
         let (sigma,c_interp) = interp_constr_may_eval ist env sigma c in
         Sigma.Unsafe.of_pair (Ftactic.return (Value.of_constr c_interp), sigma)
       end }
-  | UConstr c ->
-      Ftactic.enter { enter = begin fun gl ->
-        let env = Proofview.Goal.env gl in
-        Ftactic.return (Value.of_uconstr (interp_uconstr ist env c))
-      end }
   | TacCall (loc,r,[]) ->
       interp_ltac_reference loc true ist r
   | TacCall (loc,f,l) ->
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 3f103a290d..55941c1ca6 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -247,7 +247,6 @@ and subst_tactic_fun subst (var,body) = (var,subst_tactic subst body)
 and subst_tacarg subst = function
   | Reference r -> Reference (subst_reference subst r)
   | ConstrMayEval c -> ConstrMayEval (subst_raw_may_eval subst c)
-  | UConstr c -> UConstr (subst_glob_constr subst c)
   | TacCall (_loc,f,l) ->
       TacCall (_loc, subst_reference subst f, List.map (subst_tacarg subst) l)
   | TacFreshId _ as x -> x