diff options
| author | Pierre-Marie Pédrot | 2014-03-01 15:31:35 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-03-01 15:32:32 +0100 |
| commit | 38fa8db7bd81155deee36c0e5ff6730851a92286 (patch) | |
| tree | 76c3444cbe564e2a5bca6f13d9b9627c59fc1a2b /tactics | |
| parent | d0eb3e2cd98bbeb08db3aa32d233233569d50351 (diff) | |
Removing a fishy use of pervasive equality in Ltac backtrace printing.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 9 |
1 files changed, 3 insertions, 6 deletions
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 -> [] |