diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index c32ade38c..b9eaf53ee 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -645,10 +645,6 @@ GEXTEND Gram | "exists"; bll = opt_bindings -> TacSplit (false,bll) | IDENT "eexists"; bll = opt_bindings -> TacSplit (true,bll) - | IDENT "constructor"; n = nat_or_var; l = with_bindings -> - TacConstructor (false,n,l) - | IDENT "econstructor"; n = nat_or_var; l = with_bindings -> - TacConstructor (true,n,l) (* Equivalence relations *) | IDENT "symmetry"; "in"; cl = in_clause -> TacSymmetry cl |