coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre Courtieu <pierre.courtieu AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] pin a hypothesis in proof general/company-coq
- Date: Thu, 14 Feb 2019 17:51:40 +0100
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-it1-f182.google.com
- Ironport-phdr: 9a23:scLt3hFuuD5ywm+hThRxfp1GYnF86YWxBRYc798ds5kLTJ7zpcuwAkXT6L1XgUPTWs2DsrQY07qQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmDmwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VC+85Kl3VhDnlCYHNyY48G7JjMxwkLlbqw+lqxBm3oLYfJ2ZOP94c6jAf90VWHBBU95eWCxPAIyyb4UBAekcM+hGs4bzqEADrQenBQS2GO/j1iNEi33w0KYn0+ohCwbG3Ak4EtwUsXTbss/1NL0MXuuo0qTIyijDb+lK2Tf89ofIbw0qrPaUXbJxb8XR01MvGB3fglqMrozlIimV1vgMs2eF8uptTu2vi2s9pAFwpjij3Nsjio7Mho8MzF3P6Ct3wIEwJdKiSU57Z8apH4dXtyGAMYt5XMciQ2VytCkk17IGpJi2dzUJxpQ/3xPTdeCLfoyS7h/gVOudOyp0iXNkdb6lmhq/8lasx+vhXceuyllKtDBKktzUu3ANyRPT7s+HR+N4/ki72DaP0xnf6uBYIUwpjKbbJYMtz70umpYJvkTDGSj2mEryjKCIbEkr5u+o6+H/brXnoJ+TKZN0hxngPqgynsGzG+c1PwgUU2SG+Omx1afv8VD6TblUlvE2l7PWsJHeJcQVvK65BApV35476xa+ETimys4YkmcdIF1ZfxKHkpLpO03PIP/mEPeymFuskDJxyPDHOr3tGInCLn/GkLv5Z7Zy91ZcyBYvzdBY/59bFrYBIOvqVkDtsNzYEwQ2Phevw+fnDdV9zpkRVXiOAq+fKqPSsEWH6vghI+mWN8cpv2PWLOFtzPrzhzdtklgEOKKtwJE/aXaiH/0gLV/PMlT2hdJUKWYHpBAzBMftlUeeUDNOLyKqXq8m/Dx9A4W7F5vCS52Fj7mI3SP9FZpTMDMVQmuQGGvlIt3XE8wHbzifd4o4ymRdBOqRDrQ53BTrjzfUjr9uL+7a4Cod7Mux29185umVnhY3p2UtU5atllqVRmQxpVsmAics1fkm80N4w1aHl6N/hq4ATIEB17ZySg4/cKXk4al6BtT1AFyTe96ITBOnXozjD2hhFJQ+xNgBZ0s7ENKn3EjO
Not to my knowledge, but this is an interesting feature.
P.
Le jeu. 14 févr. 2019 à 17:12, Abhishek Anand
<abhishek.anand.iitg AT gmail.com>
a écrit :
>
> 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,
> --
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/
- [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.