aboutsummaryrefslogtreecommitdiffhomepage
path: root/lego
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <courtieu@lri.fr>2000-09-29 13:29:49 +0000
committerGravatar Pierre Courtieu <courtieu@lri.fr>2000-09-29 13:29:49 +0000
commit72ea2bfb9bd301c8b168e0c5b8bdab7bf4d3461c (patch)
tree1a66fdf516f96d5236cc71e389c7cbdddf86ed74 /lego
parent63000d541743e839c62be74af1158f241124ba42 (diff)
A little work around for the bug of Coq concerning the restart that
uses Reset Initial which doesn't reset the Implicit Arguments flag to Off (this is the bug), I added the good command to the coq reset command, this has to be backtracked when V7 will be done (the bug is already corrected in V7).
Diffstat (limited to 'lego')
0 files changed, 0 insertions, 0 deletions