diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-10 12:29:57 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-10 12:31:22 +0200 |
| commit | dcac2e58843c53137e740fc1bf324ddc16932223 (patch) | |
| tree | 586c8daf8f642f3e0418e02edbb1be31966d3232 /proofs/proof_type.ml | |
| parent | 2bb166e09d829c3d70b99d1cb9c74511e47f517e (diff) | |
Fixing localisation of tactic errors (my mistake in himsg.ml essentially).
Diffstat (limited to 'proofs/proof_type.ml')
| -rw-r--r-- | proofs/proof_type.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 76459a59a..2f0b0e608 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 |