diff options
Diffstat (limited to 'tactics/tacintern.ml')
| -rw-r--r-- | tactics/tacintern.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 84df21eb81..e69d3f61e0 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -531,9 +531,6 @@ let rec intern_atomic lf ist x = intern_hyp ist id1, intern_hyp ist id2) l) - (* Constructors *) - | TacSplit (ev,bll) -> TacSplit (ev,List.map (intern_bindings ist) bll) - (* Conversion *) | TacReduce (r,cl) -> dump_glob_red_expr r; |