From 7edfbedba1426282b69b7bc8bc01259015c27e0a Mon Sep 17 00:00:00 2001
From: ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 28 May 2013 19:18:07 +0000
Subject: Getting rid of LtacLocated exception transformer.

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

(limited to 'proofs/proof_type.ml')

diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 954e2fdb7..f7f10272c 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -58,5 +58,4 @@ type ltac_call_kind =
 
 type ltac_trace = (int * Loc.t * ltac_call_kind) list
 
-exception LtacLocated of ltac_trace * Loc.t * exn
-
+let (ltac_trace_info : (ltac_trace * Loc.t) Exninfo.t) = Exninfo.make ()
-- 
cgit v1.2.3