diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-02 15:18:42 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-02 18:34:11 +0100 |
| commit | cc153dbbe45d5cf7f6ebfef6010adcc4f5bb568c (patch) | |
| tree | 228322f5b8b359db476f9a0428da61d68c29a589 /intf | |
| parent | 7a33a6284ba4e0953f82cf436fe324cdb95497e7 (diff) | |
Dead code from August 2014 in apply in.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/tacexpr.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index eb4e5ae7d..8c55a5705 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -136,7 +136,7 @@ type 'a gen_atomic_tactic_expr = | TacIntroMove of Id.t option * 'nam move_location | TacExact of 'trm | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list * - (clear_flag * 'nam * 'dtrm intro_pattern_expr located option) option + ('nam * 'dtrm intro_pattern_expr located option) option | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option | TacCase of evars_flag * 'trm with_bindings_arg | TacFix of Id.t option * int |