diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof_type.ml | 1 | ||||
| -rw-r--r-- | proofs/proof_type.mli | 1 |
2 files changed, 2 insertions, 0 deletions
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 76459a59ac..2f0b0e6083 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -45,6 +45,7 @@ type rule = prim_rule (** Ltac traces *) type ltac_call_kind = + | LtacMLCall of glob_tactic_expr | LtacNotationCall of KerName.t | LtacNameCall of ltac_constant | LtacAtomCall of glob_atomic_tactic_expr diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index bbb2c8e09e..5fcdddeac9 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -68,6 +68,7 @@ type tactic = goal sigma -> goal list sigma (** TODO: Move those definitions somewhere sensible *) type ltac_call_kind = + | LtacMLCall of glob_tactic_expr | LtacNotationCall of KerName.t | LtacNameCall of ltac_constant | LtacAtomCall of glob_atomic_tactic_expr |