aboutsummaryrefslogtreecommitdiffhomepage
path: root/CREDITS
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2018-03-06 13:41:37 +0100
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2018-03-06 19:39:35 +0100
commit940b2f972c4b3f42850e36c721564b127d30e496 (patch)
treef78dd9dae78e3058a42d862540d5f5cf26a48d31 /CREDITS
parent8127e69a678f138ea201ec1251990b1615cb27bc (diff)
An experimental 'Show Extraction' command (grant feature wish #4129)
Attempt to extract the current ongoing proof (request by Clément Pit-Claudel on coqdev, and also #4129). Evars are handled as axioms.
Diffstat (limited to 'CREDITS')
0 files changed, 0 insertions, 0 deletions