Removing useless use of metaids in tactic AST.

8 files changed, 9 insertions, 12 deletions

diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index a52fdeb62c..cada607f67 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -83,7 +83,7 @@ let mlexpr_of_or_var f = function
   | Misctypes.ArgArg x -> <:expr< Misctypes.ArgArg $f x$ >>
   | Misctypes.ArgVar id -> <:expr< Misctypes.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >>
 
-let mlexpr_of_hyp = mlexpr_of_or_metaid (mlexpr_of_located mlexpr_of_ident)
+let mlexpr_of_hyp = (mlexpr_of_located mlexpr_of_ident)
 
 let mlexpr_of_occs = function
   | Locus.AllOccurrences -> <:expr< Locus.AllOccurrences >>
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index d5d19f2eaa..983163ec14 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -70,4 +70,4 @@ val wit_red_expr :
 
 val wit_tactic : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type
 
-val wit_clause_dft_concl :  (Names.Id.t Loc.located Tacexpr.or_metaid Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
+val wit_clause_dft_concl :  (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index d03279fc3f..01e01ff858 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -258,7 +258,7 @@ type r_pat = constr_pattern_expr
 type r_cst = reference or_by_notation
 type r_ind = reference or_by_notation
 type r_ref = reference
-type r_nam  = Id.t located or_metaid
+type r_nam  = Id.t located
 type r_lev = rlevel
 
 type raw_atomic_tactic_expr =
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 58def67b68..f70a865d77 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -215,7 +215,7 @@ GEXTEND Gram
       | "|"; mrl = LIST1 match_rule SEP "|" -> mrl ] ]
   ;
   message_token:
-    [ [ id = identref -> MsgIdent (AI id)
+    [ [ id = identref -> MsgIdent id
       | s = STRING -> MsgString s
       | n = integer -> MsgInt n ] ]
   ;
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 2003ec7f94..3142522023 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -228,10 +228,7 @@ GEXTEND Gram
   ;
   (* An identifier or a quotation meta-variable *)
   id_or_meta:
-    [ [ id = identref -> AI id
-
-      (* This is used in quotations *)
-      | id = METAIDENT -> MetaId (!@loc, id) ] ]
+    [ [ id = identref -> id ] ]
   ;
   open_constr:
     [ [ c = constr -> ((),c) ] ]
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 810a652dc0..7d138efa3d 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -218,7 +218,7 @@ module Tactic :
     val red_expr : raw_red_expr Gram.entry
     val simple_tactic : raw_atomic_tactic_expr Gram.entry
     val simple_intropattern : intro_pattern_expr located Gram.entry
-    val clause_dft_concl : Names.Id.t Loc.located Tacexpr.or_metaid Locus.clause_expr Gram.entry
+    val clause_dft_concl : Names.Id.t Loc.located Locus.clause_expr Gram.entry
     val tactic_arg : raw_tactic_arg Gram.entry
     val tactic_expr : raw_tactic_expr Gram.entry
     val binder_tactic : raw_tactic_expr Gram.entry
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 0dabe3a265..c7aff50866 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -965,7 +965,7 @@ let raw_printers =
      pr_or_by_notation pr_reference,
      pr_or_by_notation pr_reference,
      pr_reference,
-     pr_or_metaid pr_lident,
+     pr_lident,
      pr_raw_extend,
      pr_raw_alias,
      strip_prod_binders_expr,
@@ -1017,7 +1017,7 @@ let () =
     Miscprint.pr_intro_pattern;
   Genprint.register_print0
     Constrarg.wit_clause_dft_concl
-    (pr_clauses (Some true) (pr_or_metaid pr_lident))
+    (pr_clauses (Some true) (pr_lident))
     (pr_clauses (Some true) pr_lident)
     (pr_clauses (Some true) (fun id -> pr_lident (Loc.ghost,id)))
   ;
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 0bb86cbf7d..7062737382 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -106,7 +106,7 @@ let intern_hyp ist (loc,id as locid) =
   else
     Pretype_errors.error_var_not_found_loc loc id
 
-let intern_hyp_or_metaid ist id = intern_hyp ist (skip_metaid id)
+let intern_hyp_or_metaid ist id = intern_hyp ist id
 
 let intern_or_var ist = function
   | ArgVar locid -> ArgVar (intern_hyp ist locid)