aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/clenvtac.ml
diff options
context:
space:
mode:
authorGravatar aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-11-02 15:34:12 +0000
committerGravatar aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-11-02 15:34:12 +0000
commit84357f0d15a1137a4b1cc5cacb86d3af5c1ca93e (patch)
tree9d6b50c88ca6550048318ac19f74522d76b45f69 /proofs/clenvtac.ml
parent1a1ee340de86b6688a8ceeec5eaa8e76032fe3f3 (diff)
Bases tactics on an IO monad.
It allowed to restore the timeout tactics. It also prepares for the debugging mechanism to be restored. ['a IO.t] is just [unit -> 'a]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16970 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/clenvtac.ml')
0 files changed, 0 insertions, 0 deletions