diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 3 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 3 |
2 files changed, 0 insertions, 6 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index b69a6a97ac..dacfd7329a 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -495,9 +495,6 @@ GEXTEND Gram | IDENT "Existing"; IDENT "Instance"; is = identref -> VernacDeclareInstance is - | IDENT "Instantiation"; IDENT "Tactic"; ":="; tac = Tactic.tactic -> - VernacSetInstantiationTactic tac - (* Implicit *) | IDENT "Implicit"; IDENT "Arguments"; enrich = [ IDENT "Enriching" -> true | -> false ]; (local,qid,pos) = diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index e2653a9606..3502a9e86c 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -717,9 +717,6 @@ let rec pr_vernac = function | VernacDeclareInstance id -> hov 1 (str"Instance" ++ spc () ++ pr_lident id) - | VernacSetInstantiationTactic tac -> - hov 1 (str"Instantiation Tactic :=" ++ spc () ++ pr_raw_tactic tac) - (* Modules and Module Types *) | VernacDefineModule (export,m,bl,ty,bd) -> let b = pr_module_binders_list bl pr_lconstr in |