Removing the UConstr entry of the tactic_arg AST.

This was redundant with the wit_uconstr generic argument, so there was no real
point on keeping it there.

6 files changed, 3 insertions, 27 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 7366bc03e..f2a567c00 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -180,7 +180,6 @@ type 'a gen_atomic_tactic_expr =
 
 constraint 'a = <
     term:'trm;
-    utrm: 'utrm;
     dterm: 'dtrm;
     pattern:'pat;
     constant:'cst;
@@ -195,7 +194,6 @@ constraint 'a = <
 and 'a gen_tactic_arg =
   | TacGeneric     of 'lev generic_argument
   | ConstrMayEval  of ('trm,'cst,'pat) may_eval
-  | UConstr        of 'utrm
   | Reference      of 'ref
   | TacCall of Loc.t * 'ref *
       'a gen_tactic_arg list
@@ -206,7 +204,6 @@ and 'a gen_tactic_arg =
 
 constraint 'a = <
     term:'trm;
-    utrm: 'utrm;
     dterm: 'dtrm;
     pattern:'pat;
     constant:'cst;
@@ -285,7 +282,6 @@ and 'a gen_tactic_expr =
 
 constraint 'a = <
     term:'t;
-    utrm: 'utrm;
     dterm: 'dtrm;
     pattern:'p;
     constant:'c;
@@ -300,7 +296,6 @@ and 'a gen_tactic_fun_ast =
 
 constraint 'a = <
     term:'t;
-    utrm: 'utrm;
     dterm: 'dtrm;
     pattern:'p;
     constant:'c;
@@ -313,7 +308,6 @@ constraint 'a = <
 (** Globalized tactics *)
 
 type g_trm = glob_constr_and_expr
-type g_utrm = g_trm
 type g_pat = glob_constr_pattern_and_expr
 type g_cst = evaluable_global_reference and_short_name or_var
 type g_ref = ltac_constant located or_var
@@ -321,7 +315,6 @@ type g_nam  = Id.t located
 
 type g_dispatch =  <
     term:g_trm;
-    utrm:g_utrm;
     dterm:g_trm;
     pattern:g_pat;
     constant:g_cst;
@@ -343,7 +336,6 @@ type glob_tactic_arg =
 (** Raw tactics *)
 
 type r_trm = constr_expr
-type r_utrm = r_trm
 type r_pat = constr_pattern_expr
 type r_cst = reference or_by_notation
 type r_ref = reference
@@ -352,7 +344,6 @@ type r_lev = rlevel
 
 type r_dispatch =  <
     term:r_trm;
-    utrm:r_utrm;
     dterm:r_trm;
     pattern:r_pat;
     constant:r_cst;
@@ -374,7 +365,6 @@ type raw_tactic_arg =
 (** Interpreted tactics *)
 
 type t_trm = Term.constr
-type t_utrm = Glob_term.closed_glob_constr
 type t_pat = constr_pattern
 type t_cst = evaluable_global_reference
 type t_ref = ltac_constant located
@@ -382,7 +372,6 @@ type t_nam  = Id.t
 
 type t_dispatch =  <
     term:t_trm;
-    utrm:t_utrm;
     dterm:g_trm;
     pattern:t_pat;
     constant:t_cst;
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index b76f5dda2..4da32c9b2 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -28,6 +28,7 @@ let arg_of_expr = function
 let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) ()
 let genarg_of_int n = in_gen (rawwit Stdarg.wit_int) n
 let genarg_of_ipattern pat = in_gen (rawwit Constrarg.wit_intro_pattern) pat
+let genarg_of_uconstr c = in_gen (rawwit Constrarg.wit_uconstr) c
 
 let reference_to_id = function
   | Libnames.Ident (loc, id) -> (loc, id)
@@ -146,7 +147,7 @@ GEXTEND Gram
   ;
   (* Can be used as argument and at toplevel in tactic expressions. *)
   tactic_top_or_arg:
-    [ [ IDENT "uconstr"; ":"; "("; c = Constr.lconstr; ")" -> UConstr c
+    [ [ IDENT "uconstr"; ":"; "("; c = Constr.lconstr; ")" -> TacGeneric (genarg_of_uconstr c)
       | IDENT "constr"; ":"; "("; c = Constr.lconstr; ")" -> ConstrMayEval (ConstrTerm c)
       | IDENT "ltac"; ":"; "("; a = tactic_expr LEVEL "5"; ")" -> arg_of_expr a
       | IDENT "ltac"; ":"; "("; n = natural; ")" -> TacGeneric (genarg_of_int n)
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 36863906e..fdc1288ae 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -696,7 +696,6 @@ module Make
   type 'a printer = {
     pr_tactic    : tolerability -> 'tacexpr -> std_ppcmds;
     pr_constr    : 'trm -> std_ppcmds;
-    pr_uconstr   : 'utrm -> std_ppcmds;
     pr_lconstr   : 'trm -> std_ppcmds;
     pr_dconstr   : 'dtrm -> std_ppcmds;
     pr_pattern   : 'pat -> std_ppcmds;
@@ -711,7 +710,6 @@ module Make
 
   constraint 'a = <
       term      :'trm;
-      utrm      :'utrm;
       dterm     :'dtrm;
       pattern   :'pat;
       constant  :'cst;
@@ -1153,8 +1151,6 @@ module Make
             pr.pr_reference r
           | ConstrMayEval c ->
             pr_may_eval pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c
-          | UConstr c ->
-            keyword "uconstr:" ++ pr.pr_uconstr c
           | TacFreshId l ->
             keyword "fresh" ++ pr_fresh_ids l
           | TacPretype c ->
@@ -1182,7 +1178,6 @@ module Make
     let pr = {
       pr_tactic = pr_raw_tactic_level;
       pr_constr = pr_constr_expr;
-      pr_uconstr = pr_constr_expr;
       pr_dconstr = pr_constr_expr;
       pr_lconstr = pr_lconstr_expr;
       pr_pattern = pr_constr_pattern_expr;
@@ -1213,7 +1208,6 @@ module Make
       let pr = {
         pr_tactic = prtac;
         pr_constr = pr_and_constr_expr (pr_glob_constr_env env);
-        pr_uconstr = pr_and_constr_expr (pr_glob_constr_env env);
         pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env);
         pr_lconstr = pr_and_constr_expr (pr_lglob_constr_env env);
         pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env);
@@ -1255,7 +1249,6 @@ module Make
       let pr = {
         pr_tactic = pr_glob_tactic_level env;
         pr_constr = pr_constr_env env Evd.empty;
-        pr_uconstr = pr_closed_glob_env env Evd.empty;
         pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env);
         pr_lconstr = pr_lconstr_env env Evd.empty;
         pr_pattern = pr_constr_pattern_env env Evd.empty;
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index a069fd755..89dc843cb 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 1a8a95158..bf5f9ddc8 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 3f103a290..55941c1ca 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