aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/auto.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-12-27 19:27:52 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-12-27 19:39:43 +0100
commit1ec0928ebecc8fa51022b681d32665d4f010e0ef (patch)
tree405ebadc827fc916f0a356884c53ec708846447c /tactics/auto.mli
parentcbd815a289db52f58235f23f5afba3be49cc8eed (diff)
Factorizing code for untyped constr evaluation.
Diffstat (limited to 'tactics/auto.mli')
0 files changed, 0 insertions, 0 deletions