diff options
| author | Hugo Herbelin | 2014-09-10 12:29:57 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-09-10 12:31:22 +0200 |
| commit | dcac2e58843c53137e740fc1bf324ddc16932223 (patch) | |
| tree | 586c8daf8f642f3e0418e02edbb1be31966d3232 /proofs | |
| parent | 2bb166e09d829c3d70b99d1cb9c74511e47f517e (diff) | |
Fixing localisation of tactic errors (my mistake in himsg.ml essentially).
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 |