From 38fa8db7bd81155deee36c0e5ff6730851a92286 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 1 Mar 2014 15:31:35 +0100
Subject: Removing a fishy use of pervasive equality in Ltac backtrace
 printing.

---
 tactics/tacinterp.ml | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index ca2c914853..c802ae984c 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -174,12 +174,9 @@ let valueIn t = TacDynamic (Loc.ghost, value_in t)
 
 (** Generic arguments : table of interpretation functions *)
 
-let push_trace (loc, ck) ist = match TacStore.get ist.extra f_trace with
-| None -> [1, loc, ck]
-| Some trace ->
-  match trace with
-  | (n,loc',ck')::trl when Pervasives.(=) ck ck' -> (n+1,loc,ck)::trl (** FIXME *)
-  | trl -> (1,loc,ck)::trl
+let push_trace call ist = match TacStore.get ist.extra f_trace with
+| None -> [call]
+| Some trace -> call :: trace
 
 let extract_trace ist = match TacStore.get ist.extra f_trace with
 | None -> []
-- 
cgit v1.2.3