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