diff options
Diffstat (limited to 'proofs/proof_type.ml')
| -rw-r--r-- | proofs/proof_type.ml | 33 |
1 files changed, 0 insertions, 33 deletions
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index b84b6db48..e09d72e47 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -46,39 +46,6 @@ type prim_rule = type rule = prim_rule -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 = |