Removing a fishy use of pervasive equality in Ltac backtrace printing.

4 files changed, 38 insertions, 45 deletions

diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index c04c44193e..4394aeff1d 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -55,6 +55,6 @@ type ltac_call_kind =
   | LtacVarCall of Id.t * glob_tactic_expr
   | LtacConstrInterp of glob_constr * Pretyping.ltac_var_map
 
-type ltac_trace = (int * Loc.t * ltac_call_kind) list
+type ltac_trace = (Loc.t * ltac_call_kind) list
 
 let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make ()
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 8cc6bf76f6..4abd6f7762 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -82,6 +82,6 @@ type ltac_call_kind =
   | LtacVarCall of Id.t * glob_tactic_expr
   | LtacConstrInterp of glob_constr * Pretyping.ltac_var_map
 
-type ltac_trace = (int * Loc.t * ltac_call_kind) list
+type ltac_trace = (Loc.t * ltac_call_kind) list
 
 val ltac_trace_info : ltac_trace Exninfo.t
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 -> []
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 1cbb47846c..5d024d31c5 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -1149,61 +1149,57 @@ let explain_reduction_tactic_error = function
 
 let is_defined_ltac trace =
   let rec aux = function
-  | (_,_,Proof_type.LtacNameCall _) :: tail -> true
-  | (_,_,Proof_type.LtacAtomCall _) :: tail -> false
+  | (_, Proof_type.LtacNameCall _) :: tail -> true
+  | (_, Proof_type.LtacAtomCall _) :: tail -> false
   | _ :: tail -> aux tail
   | [] -> false in
   aux (List.rev trace)
 
-let explain_ltac_call_trace (nrep,last,trace,loc) =
-  let calls =
-    (nrep,last) :: List.rev_map (fun(n,_,ck)->(n,ck)) trace
+let explain_ltac_call_trace last trace loc =
+  let calls = last :: List.rev_map snd trace in
+  let pr_call ck = match ck with
+  | Proof_type.LtacNotationCall kn -> quote (KerName.print kn)
+  | Proof_type.LtacNameCall cst -> quote (Pptactic.pr_ltac_constant cst)
+  | Proof_type.LtacVarCall (id,t) ->
+      quote (Nameops.pr_id id) ++ strbrk " (bound to " ++
+        Pptactic.pr_glob_tactic (Global.env()) t ++ str ")"
+  | Proof_type.LtacAtomCall te ->
+      quote (Pptactic.pr_glob_tactic (Global.env())
+              (Tacexpr.TacAtom (Loc.ghost,te)))
+  | Proof_type.LtacConstrInterp (c,(vars,unboundvars)) ->
+      quote (pr_glob_constr_env (Global.env()) c) ++
+        (if not (Id.Map.is_empty vars) then
+          strbrk " (with " ++
+            prlist_with_sep pr_comma
+            (fun (id,c) ->
+                pr_id id ++ str ":=" ++ Printer.pr_lconstr_under_binders c)
+            (List.rev (Id.Map.bindings vars)) ++ str ")"
+        else mt())
   in
-  let pr_call (n,ck) =
-    (match ck with
-       | Proof_type.LtacNotationCall kn -> quote (KerName.print kn)
-       | Proof_type.LtacNameCall cst -> quote (Pptactic.pr_ltac_constant cst)
-       | Proof_type.LtacVarCall (id,t) ->
-	   quote (Nameops.pr_id id) ++ strbrk " (bound to " ++
-	     Pptactic.pr_glob_tactic (Global.env()) t ++ str ")"
-       | Proof_type.LtacAtomCall te ->
-	   quote (Pptactic.pr_glob_tactic (Global.env())
-		    (Tacexpr.TacAtom (Loc.ghost,te)))
-       | Proof_type.LtacConstrInterp (c,(vars,unboundvars)) ->
-	   quote (pr_glob_constr_env (Global.env()) c) ++
-	     (if not (Id.Map.is_empty vars) then
-		strbrk " (with " ++
-		  prlist_with_sep pr_comma
-		  (fun (id,c) ->
-		     pr_id id ++ str ":=" ++ Printer.pr_lconstr_under_binders c)
-		  (List.rev (Id.Map.bindings vars)) ++ str ")"
-	      else mt())) ++
-      (if Int.equal n 2 then str " (repeated twice)"
-       else if n>2 then str " (repeated "++int n++str" times)"
-       else mt()) in
-    if not (List.is_empty calls) then
-      let kind_of_last_call = match List.last calls with
-    | (_,Proof_type.LtacConstrInterp _) -> ", last term evaluation failed."
-    | _ -> ", last call failed." in
+  match calls with
+  | [] -> mt ()
+  | _ ->
+    let kind_of_last_call = match List.last calls with
+    | Proof_type.LtacConstrInterp _ -> ", last term evaluation failed."
+    | _ -> ", last call failed."
+    in
     hov 0 (str "In nested Ltac calls to " ++
            pr_enum pr_call calls ++ strbrk kind_of_last_call)
-  else
-    mt ()
 
 let skip_extensions trace =
   let rec aux = function
-  | (_,_,Proof_type.LtacAtomCall
+  | (_,Proof_type.LtacAtomCall
       (Tacexpr.TacAlias _ | Tacexpr.TacExtend _) as tac) :: tail -> [tac]
   | _ :: tail -> aux tail
   | [] -> [] in
   List.rev (aux (List.rev trace))
 
 let extract_ltac_trace trace eloc =
-  let (nrep,loc,c),tail = List.sep_last trace in
+  let (loc,c),tail = List.sep_last trace in
   if is_defined_ltac trace then
     (* We entered a user-defined tactic,
        we display the trace with location of the call *)
-    let msg = hov 0 (explain_ltac_call_trace (nrep,c,tail,eloc) ++ fnl()) in
+    let msg = hov 0 (explain_ltac_call_trace c tail eloc ++ fnl()) in
     Some msg, loc
   else
     (* We entered a primitive tactic, we don't display trace but
@@ -1212,7 +1208,7 @@ let extract_ltac_trace trace eloc =
       if not (Loc.is_ghost eloc) then eloc else
         (* trace is with innermost call coming first *)
         let rec aux = function
-        | (_,loc,_)::tail when not (Loc.is_ghost loc) -> loc
+        | (loc,_)::tail when not (Loc.is_ghost loc) -> loc
         | _::tail -> aux tail
         | [] -> Loc.ghost in
         aux (skip_extensions trace) in