aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/eauto.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-03-06 18:34:39 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-03-06 18:54:04 +0100
commit6ecbc9990a49a0dd51970c7fc8b13f39f02be773 (patch)
tree027928408f8e28263edf98a5bd58cd96d43dffca /tactics/eauto.ml
parentd3653c6da5770dfc4d439639b49193e30172763a (diff)
Moving Ltac traces to Tacexpr and Tacinterp.
Diffstat (limited to 'tactics/eauto.ml')
0 files changed, 0 insertions, 0 deletions