From 97fc36f552bfd9731ac47716faf2b02d4555eb07 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 17 Feb 2013 14:55:59 +0000
Subject: Revised the Ltac trace mechanism so that trace breaking due to
 interleaving of ltac and ml code is not visible (this particularly applies to
 ltac notation ring, which calls ml-level ring_lookup and Ring again at the
 ltac level, resulting in non-localisation of "ring" errors).

Added also missing LtacLocated checks in Class_instance and Proofview.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16204 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/proof_type.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs/proof_type.ml')

diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index eadf870fb4..af50059b8d 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -57,5 +57,5 @@ type ltac_call_kind =
 
 type ltac_trace = (int * Loc.t * ltac_call_kind) list
 
-exception LtacLocated of (int * ltac_call_kind * ltac_trace * Loc.t) * exn
+exception LtacLocated of ltac_trace * Loc.t * exn
 
-- 
cgit v1.2.3