search

cpitclaudel / company-coq

A Coq IDE build on top of Proof General's Coq mode
GNU General Public License v3.0
349 stars 30 forks source link

How do I get a unification diff from console emacs? #153

Open JasonGross opened 7 years ago

JasonGross commented 7 years ago

On something like this: image

Unable to unify
 "wff (flatten_binding_list ?M1499 ?M1500)
    (smart_interp_flat_map (fun (t : base_type_code) (x : exprf base_type_code op (Tbase t)) => x) ()%expr
       (fun (A B : flat_type base_type_code) (x : exprf base_type_code op A) (y : exprf base_type_code op B) => (x, y))
       (SmartFlatTypeMapUnInterp2
          (fun (t : base_type_code) (bs : interp_base_type_bounds t) (v : exprf base_type_code op (Tbase (bound_base_type t bs))) =>
....

How do I get the diff without mouse access? Hitting RET around (diff) gives Buffer is read-only: #<buffer *response*>, and using M-x company-coq-diff-unification-error gives No unification error message found.

cpitclaudel commented 7 years ago

Does that work in non-console emacs?