aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/taccoerce.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-02-15 15:17:05 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-02-15 15:31:14 +0100
commit4ea9b3193eaced958bb277c0723fb54d661ff520 (patch)
tree674fe651612dc17f3bf99404fae02d58437ef5a1 /tactics/taccoerce.ml
parent15b28f0ae1e31506f3fb153fc6e50bc861717eb9 (diff)
More conversion functions in the new tactic API.
Diffstat (limited to 'tactics/taccoerce.ml')
0 files changed, 0 insertions, 0 deletions