diff options
Diffstat (limited to 'proofs/proof_type.mli')
| -rw-r--r-- | proofs/proof_type.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index f7cd8ad87d..8cc6bf76f6 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -76,7 +76,7 @@ type tactic = goal sigma -> goal list sigma (** TODO: Move those definitions somewhere sensible *) type ltac_call_kind = - | LtacNotationCall of string + | LtacNotationCall of KerName.t | LtacNameCall of ltac_constant | LtacAtomCall of glob_atomic_tactic_expr | LtacVarCall of Id.t * glob_tactic_expr |