diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-24 10:07:57 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-24 10:25:22 +0100 |
| commit | ee162ba3b28fccca0a2b3ea4b1e0811006840570 (patch) | |
| tree | d35af1820687bc62c6369c832533f79eb15e0a1d /parsing | |
| parent | 0a024252f6346287cf4886903c800590191ddec0 (diff) | |
Removing the MetaIdArg entry of tactic expressions.
This was historically used together with the <:tactic< ... >> quotation to insert
foreign code as $foo, but it actually only survived in the implementation of Tauto.
With the removal of the quotation feature, this is now totally obsolete.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_ltac.ml4 | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 12d53030d..0a11d3928 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -146,7 +146,6 @@ GEXTEND Gram | r = reference -> Reference r | c = Constr.constr -> ConstrMayEval (ConstrTerm c) (* Unambigous entries: tolerated w/o "ltac:" modifier *) - | id = METAIDENT -> MetaIdArg (!@loc,true,id) | "()" -> TacGeneric (genarg_of_unit ()) ] ] ; (* Can be used as argument and at toplevel in tactic expressions. *) @@ -179,8 +178,7 @@ GEXTEND Gram | c = Constr.constr -> ConstrTerm c ] ] ; tactic_atom: - [ [ id = METAIDENT -> MetaIdArg (!@loc,true,id) - | n = integer -> TacGeneric (genarg_of_int n) + [ [ n = integer -> TacGeneric (genarg_of_int n) | r = reference -> TacCall (!@loc,r,[]) | "()" -> TacGeneric (genarg_of_unit ()) ] ] ; |