diff options
Diffstat (limited to 'proofs/proof_type.mli')
| -rw-r--r-- | proofs/proof_type.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index f835e2ef4..c06aff7e1 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -98,7 +98,7 @@ and tactic = goal sigma -> (goal list sigma * validation) and validation = (proof_tree list -> proof_tree) and tactic_expr = - (constr, + (open_constr, constr_pattern, evaluable_global_reference, inductive, @@ -108,7 +108,7 @@ and tactic_expr = Tacexpr.gen_tactic_expr and atomic_tactic_expr = - (constr, + (open_constr, constr_pattern, evaluable_global_reference, inductive, @@ -118,7 +118,7 @@ and atomic_tactic_expr = Tacexpr.gen_atomic_tactic_expr and tactic_arg = - (constr, + (open_constr, constr_pattern, evaluable_global_reference, inductive, |