diff options
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 -> [] |