From dcac2e58843c53137e740fc1bf324ddc16932223 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 10 Sep 2014 12:29:57 +0200
Subject: Fixing localisation of tactic errors (my mistake in himsg.ml
 essentially).

---
 proofs/proof_type.ml  | 1 +
 proofs/proof_type.mli | 1 +
 2 files changed, 2 insertions(+)

(limited to 'proofs')

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
-- 
cgit v1.2.3