From 52aff80a4736ccaeb8610185959affb516a6bd9f Mon Sep 17 00:00:00 2001
From: barras
Date: Wed, 4 Mar 2009 18:45:10 +0000
Subject: commande Timeout + compaction des traces de debug_tactic

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11959 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/proof_type.ml  | 4 ++--
 proofs/proof_type.mli | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'proofs')

diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index dabc84ca31..5bd8060ae1 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -102,8 +102,8 @@ type ltac_call_kind =
   | LtacConstrInterp of rawconstr *
       ((identifier * constr) list * (identifier * identifier option) list)
 
-type ltac_trace = (loc * ltac_call_kind) list
+type ltac_trace = (int * loc * ltac_call_kind) list
 
-exception LtacLocated of (ltac_call_kind * ltac_trace * loc) * exn
+exception LtacLocated of (int * ltac_call_kind * ltac_trace * loc) * exn
 
 let abstract_tactic_box = ref (ref None)
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 1529a07f37..0bd0eaa113 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -137,8 +137,8 @@ type ltac_call_kind =
   | LtacConstrInterp of rawconstr *
       ((identifier * constr) list * (identifier * identifier option) list)
 
-type ltac_trace = (loc * ltac_call_kind) list
+type ltac_trace = (int * loc * ltac_call_kind) list
 
-exception LtacLocated of (ltac_call_kind * ltac_trace * loc) * exn
+exception LtacLocated of (int * ltac_call_kind * ltac_trace * loc) * exn
 
 val abstract_tactic_box : atomic_tactic_expr option ref ref
-- 
cgit v1.2.3