{"action":"created","issue":{"url":"https://api.github.com/repos/cpitclaudel/company-coq/issues/22","labels_url":"https://api.github.com/repos/cpitclaudel/company-coq/issues/22/labels{/name}","comments_url":"https://api.github.com/repos/cpitclaudel/company-coq/issues/22/comments","events_url":"https://api.github.com/repos/cpitclaudel/company-coq/issues/22/events","html_url":"https://github.com/cpitclaudel/company-coq/issues/22","id":105040997,"number":22,"title":"Company: Front-end company-pseudo-tooltip-unless-just-one-frontend error \"Wrong type argument: number-or-marker-p, nil\" on command post-command","user":{"login":"JasonGross","id":396076,"avatar_url":"https://avatars.githubusercontent.com/u/396076?v=3","gravatar_id":"","url":"https://api.github.com/users/JasonGross","html_url":"https://github.com/JasonGross","followers_url":"https://api.github.com/users/JasonGross/followers","following_url":"https://api.github.com/users/JasonGross/following{/other_user}","gists_url":"https://api.github.com/users/JasonGross/gists{/gist_id}","starred_url":"https://api.github.com/users/JasonGross/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/JasonGross/subscriptions","organizations_url":"https://api.github.com/users/JasonGross/orgs","repos_url":"https://api.github.com/users/JasonGross/repos","events_url":"https://api.github.com/users/JasonGross/events{/privacy}","received_events_url":"https://api.github.com/users/JasonGross/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":2,"created_at":"2015-09-05T18:13:32Z","updated_at":"2015-09-05T18:58:22Z","closed_at":null,"body":"![screenshot from 2015-09-05 14 08 04](https://cloud.githubusercontent.com/assets/396076/9700627/a4eb6912-53d7-11e5-9973-d29ccaf52a0d.png)\r\n\r\nAfter updating all of my emacs packages just now, I pasted the code at the bottom into a fresh emacs buffer `/tmp/foo5.v` (with the Edit->Paste terminal menu), and then pressed the down arrow key while emacs was pasting.  This is emacs inside ssh inside screen inside ssh.  Holding down `C-g` killed it after a while.\r\n\r\nIs it possible to make company-coq not try to do anything complicated while pasting code?\r\n\r\nPasted code:\r\n```coq\r\nRequire Coq.Lists.List.\r\nGlobal Set Implicit Arguments.\r\nImport Coq.Lists.List.\r\nClass IndexBound {A : Set} (a : A) (Bound : list A) :=\r\n  { ibound :> nat;\r\n    boundi : nth_error Bound ibound = Some a}.\r\nGlobal Arguments ibound {A} [a Bound] _ .\r\nGlobal Arguments boundi {A} [a Bound] _.\r\nRecord BoundedIndex {A : Set} (Bound : list A) :=\r\n  { bindex : A;\r\n    indexb :> IndexBound bindex Bound }.\r\n\r\nContext {A : Type} {C : Set}.\r\nVariable (projAC : A -> C).\r\nAxiom None_neq_Some : forall (AnyT AnyT' : Type) (a : AnyT), None = Some a -> AnyT'.\r\n\r\nDefinition nth_Bounded'\r\n           (Bound : list A)\r\n           (c : C)\r\n           (a_opt : option A)\r\n           (nth_n : option_map projAC a_opt = Some c)\r\n: A := match a_opt as x\r\n             return (option_map projAC x = Some c) -> A with\r\n         | Some a => fun _ => a\r\n         | None => fun f => None_neq_Some _ f\r\n       end nth_n.\r\n\r\nAxiom nth_error_map : forall n As c_opt, nth_error (map projAC As) n = c_opt -> option_map projAC (nth_error As n) = c_opt.\r\n\r\nDefinition nth_Bounded\r\n           (Bound : list A)\r\n           (idx : BoundedIndex (map projAC Bound))\r\n: A := nth_Bounded' Bound (nth_error Bound (ibound idx))\r\n                    (nth_error_map _ _ (boundi idx)).\r\n\r\nProgram Definition nth_Bounded_ind2\r\n        (P : forall As, BoundedIndex (map projAC As)\r\n                        -> BoundedIndex (map projAC As)\r\n                        -> A -> A -> Prop)\r\n: forall (Bound : list A)\r\n         (idx : BoundedIndex (map projAC Bound))\r\n         (idx' : BoundedIndex (map projAC Bound)),\r\n    match nth_error Bound (ibound idx), nth_error Bound (ibound idx') with\r\n      | Some a, Some a' => P Bound idx idx' a a'\r\n      | _, _ => True\r\n    end\r\n    -> P Bound idx idx' (nth_Bounded _ idx) (nth_Bounded _ idx'):=\r\n  fun Bound idx idx' =>\r\n    match (nth_error Bound (ibound idx)) as e, (nth_error Bound (ibound idx')) as e'\r\n          return\r\n          (forall (f : option_map _ e = Some (bindex idx))\r\n                  (f' : option_map _ e' = Some (bindex idx')),\r\n             (match e, e' with\r\n                | Some a, Some a' => P Bound idx idx' a a'\r\n                | _, _ => True\r\n              end)\r\n             -> P Bound idx idx'\r\n                  (match e as e'' return\r\n                         option_map _ e'' = Some (bindex idx)\r\n                         -> A\r\n                   with\r\n                     | Some a => fun _ => a\r\n                     | _ => fun f => _\r\n                   end f)\r\n                  (match e' as e'' return\r\n                         option_map _ e'' = Some (bindex idx')\r\n                         -> A\r\n                   with\r\n                     | Some a => fun _ => a\r\n                     | _ => fun f => _\r\n                   end f')) with\r\n      | Some a, Some a' => fun _ _ H => _\r\n      | _, _ => fun f => _\r\n    end (nth_error_map _ _ (boundi idx))\r\n        (nth_error_map _ _ (boundi idx')).\r\n\r\nLemma nth_Bounded_eq\r\n: forall (Bound : list A)\r\n         (idx idx' : BoundedIndex (map projAC Bound)),\r\n    ibound idx = ibound idx'\r\n    -> nth_Bounded Bound idx = nth_Bounded Bound idx'.\r\nProof.\r\n  intros.\r\n  eapply nth_Bounded_ind2 with (idx := idx) (idx' := idx').\r\n  simpl.\r\n  pattern (nth_error Bound (ibound idx')); case_eq (nth_error Bound (ibound idx')) || fail \"too early\".\r\n  Undo.\r\n  unfold Exc; case_eq (nth_error Bound (ibound idx')) || fail \"too early\".\r\n  Undo.\r\n  case_eq (nth_error Bound (ibound idx')).\r\n```\r\n\r\n\r\nIf I spam `C-g`, it seems to consistently end up at `    -> P Bou` in `Program Definition nth_Bounded_ind2`."},"comment":{"url":"https://api.github.com/repos/cpitclaudel/company-coq/issues/comments/137986774","html_url":"https://github.com/cpitclaudel/company-coq/issues/22#issuecomment-137986774","issue_url":"https://api.github.com/repos/cpitclaudel/company-coq/issues/22","id":137986774,"user":{"login":"JasonGross","id":396076,"avatar_url":"https://avatars.githubusercontent.com/u/396076?v=3","gravatar_id":"","url":"https://api.github.com/users/JasonGross","html_url":"https://github.com/JasonGross","followers_url":"https://api.github.com/users/JasonGross/followers","following_url":"https://api.github.com/users/JasonGross/following{/other_user}","gists_url":"https://api.github.com/users/JasonGross/gists{/gist_id}","starred_url":"https://api.github.com/users/JasonGross/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/JasonGross/subscriptions","organizations_url":"https://api.github.com/users/JasonGross/orgs","repos_url":"https://api.github.com/users/JasonGross/repos","events_url":"https://api.github.com/users/JasonGross/events{/privacy}","received_events_url":"https://api.github.com/users/JasonGross/received_events","type":"User","site_admin":false},"created_at":"2015-09-05T18:58:22Z","updated_at":"2015-09-05T18:58:22Z","body":"The bug is consistently reproducible the 2-3 times that I tried it (and I just tried again now, though I had to wait about 20 seconds before it showed up).  It shows that error message repeatedly (it keeps flashing between that, and something else I can't read).  It \"freezes\" emacs in the sense that I can't switch to another file, but if I spam `C-g` enough, it stops, and the text up to `-> P Bou` shows up, and then I can do other things.  I'm using PG 4.3pre131011."}}