diff options
| author | Pierre-Marie Pédrot | 2014-08-24 20:55:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-08-24 20:55:53 +0200 |
| commit | 965be8e6c441214542947b75e1625bc9068c40c9 (patch) | |
| tree | 73d6660068345d6e3b331ca60c42eafabca1cfcb | |
| parent | f4b0851f759ebbc467886372f7b0d5c9a1ccd173 (diff) | |
Removing a unused legacy parsing rule.
| -rw-r--r-- | parsing/g_ltac.ml4 | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index ce3105548d..faea9baddf 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -104,8 +104,6 @@ GEXTEND Gram | IDENT "external"; com = STRING; req = STRING; la = LIST1 tactic_arg -> TacArg (!@loc,TacExternal (!@loc,com,req,la)) | st = simple_tactic -> st - | IDENT "constr"; ":"; id = METAIDENT -> - TacArg(!@loc,MetaIdArg (!@loc,false,id)) | IDENT "constr"; ":"; c = Constr.constr -> TacArg(!@loc,ConstrMayEval(ConstrTerm c)) | a = tactic_top_or_arg -> TacArg(!@loc,a) |