diff options
Diffstat (limited to 'proofs/proof_type.mli')
| -rw-r--r-- | proofs/proof_type.mli | 34 |
1 files changed, 0 insertions, 34 deletions
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 6688d6e62..95ca33e90 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -70,40 +70,6 @@ type goal = Goal.goal type tactic = goal sigma -> goal list sigma - -type tactic_expr = - (constr, - constr_pattern, - evaluable_global_reference, - inductive, - ltac_constant, - identifier, - glob_tactic_expr, - tlevel) - Tacexpr.gen_tactic_expr - -and atomic_tactic_expr = - (constr, - constr_pattern, - evaluable_global_reference, - inductive, - ltac_constant, - identifier, - glob_tactic_expr, - tlevel) - Tacexpr.gen_atomic_tactic_expr - -and tactic_arg = - (constr, - constr_pattern, - evaluable_global_reference, - inductive, - ltac_constant, - identifier, - glob_tactic_expr, - tlevel) - Tacexpr.gen_tactic_arg - (** Ltac traces *) type ltac_call_kind = |