The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq users,

 

I just spent an hour debugging some Ltac scripts, which worked perfectly fine until I added a  “Require Import Omega”.

 

The problem was that Omega defines an operator “=?” after which Ltac expressions like

 

match goal with |- ?x=?y

 

parse as

 

                match goal with |- ?x  =?  y

 

rather than

 

                match goal with |- ?x  =  ?y

 

as without omega, which leads to rather strange effects. The easy fix is to add a space after the =.

 

I hope it helps someone to avoid falling into the same pit.

 

Best regards,

 

Michael