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 b905c0a26b..c8b4fc3ea1 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -71,7 +71,7 @@ and tactic_expr = (constr, constr_pattern, evaluable_global_reference, - inductive or_metanum, + inductive, ltac_constant, identifier, glob_tactic_expr) @@ -81,7 +81,7 @@ and atomic_tactic_expr = (constr, constr_pattern, evaluable_global_reference, - inductive or_metanum, + inductive, ltac_constant, identifier, glob_tactic_expr) @@ -91,7 +91,7 @@ and tactic_arg = (constr, constr_pattern, evaluable_global_reference, - inductive or_metanum, + inductive, ltac_constant, identifier, glob_tactic_expr) |