coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] pin a hypothesis in proof general/company-coq
- Date: Thu, 14 Feb 2019 08:12:13 -0800
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-yb1-f176.google.com
- Ironport-phdr: 9a23:tEZNGBTrTi300xov71UZrdzWptpsv+yvbD5Q0YIujvd0So/mwa69bRON2/xhgRfzUJnB7Loc0qyK6/CmATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfbB/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/27XhMJ+j6xVvQyvqABkzoHOfI2YLuBzcr/Bcd4YQ2dKQ8ZfVzZGAoO5d4YCE/EOPeZZr4nmp1sBsxi+DhSwCePp0DBIgGL51rA93us7Cg7G3A0gH8kOsHvKr9X5Lr0dUeavw6nO0DrPdfJW2Tbh6IjHaR0hrvSMUqhxccrV00UgCwTFjlCJpIHjIjib2OMNs22B4OphU+Kik3IoqwZrojip2Mgsjo3JipgLxV/Z6CV0xps+K96gSENjf9KoDJ9duzuZOoZ2WM8uXXxktSIgxrEbu5O2fS4Hw4k9yRHFcfyIaY2I7wrjVOmPJTd4g2poeLeliBaz9Uis0+39WdKp3FpToCpJj9vBu3EX2xzc7ciHTfR9/kO/1jqVyw/T7eRELVg1lardNZEh3qY9moQPvUnHBCP7m0X7gLWIekk5/uWk8fnrb7fnq5OEMo97kAD+MqAgmsylBuQ4NxADUHKA9uS81b3j5k35T6tJjvEsiKbZtorVJcIGqaKjAg9V05oj6xmkAjep1dQXh3gHLFZfdB2biIjpPknCIOrkAvenn1SsjDBryujaMb3mG5XBN2TMkLP8fblm8ENc0woyzdVH551OEL0BIfTzWlXwtNPCFBM5PRa0kK7bD4B20ZpbUmaSCOfNO6TL9FSM++gHIu+WZYZTtiyreNY/4Pu7pHU5mEQdcKrh9J0ebnzwSv1sI0SCYXfvxN4HGGEG+As/UOPCh1iLUDoVbHG3CfFvrgonAZ6rWN+QDrumh6aMiX/iT89mI1teA1XJKk/GMoCNWvMCciWXe5YznTkNVLznQIgkh0j36F3KjoF/J++RwRU28Ir53YEsteLWnBA2szdzCpbFijzffyRPhmoNAgQO8uV/rEh6kAnR1KF5h7lJH4UW6aoWDEE1MpnTy+E8ANf3CFrM
In proof general/company-coq, is there a way to "pin a hypothesis" so that it remains in view in the proof state (goals) frame.
-- Currently, at each step, the frame always scrolls all the way down to put the conclusion in view.
Thanks,
- [Coq-Club] pin a hypothesis in proof general/company-coq, Abhishek Anand, 02/14/2019
- Re: [Coq-Club] pin a hypothesis in proof general/company-coq, Pierre Courtieu, 02/14/2019
Archive powered by MHonArc 2.6.18.