diff options
| author |  Jason Gross <jagro@google.com> | 2016-09-02 13:15:40 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-09-02 13:15:40 -0700 |
| commit | 98b221aa42982f00bf43ba65811b278e6a45c92c (patch) | |
| tree | ba07d761832e156993f06900809de285ec3b945d /src/Util/Tactics.v | |
| parent | e181217f5df30e0447239fb2f3d2b0048621b63d (diff) | |
Strip <infomsg>; it messes things up in Coq 8.6 display
Diffstat (limited to 'src/Util/Tactics.v')
| -rw-r--r-- | src/Util/Tactics.v | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index 6f2c407f5..18abc1b28 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -436,20 +436,19 @@ Ltac simplify_projections := (** constr-based [idtac] *) Class cidtac {T} (msg : T) := Build_cidtac : True. -(** Include "infomsg" tags so that messages show up better in Coq 8.4 + PG *) -Hint Extern 0 (cidtac ?msg) => idtac "<infomsg>" msg "</infomsg>"; exact I : typeclass_instances. +Hint Extern 0 (cidtac ?msg) => idtac msg; exact I : typeclass_instances. (** constr-based [idtac] *) Class cidtac2 {T1 T2} (msg1 : T1) (msg2 : T2) := Build_cidtac2 : True. -Hint Extern 0 (cidtac2 ?msg1 ?msg2) => idtac "<infomsg>" msg1 msg2 "</infomsg>"; exact I : typeclass_instances. +Hint Extern 0 (cidtac2 ?msg1 ?msg2) => idtac msg1 msg2; exact I : typeclass_instances. Class cidtac3 {T1 T2 T3} (msg1 : T1) (msg2 : T2) (msg3 : T3) := Build_cidtac3 : True. -Hint Extern 0 (cidtac3 ?msg1 ?msg2 ?msg3) => idtac "<infomsg>" msg1 msg2 msg3 "</infomsg>"; exact I : typeclass_instances. +Hint Extern 0 (cidtac3 ?msg1 ?msg2 ?msg3) => idtac msg1 msg2 msg3; exact I : typeclass_instances. Class cfail {T} (msg : T) := Build_cfail : True. -Hint Extern 0 (cfail ?msg) => idtac "<infomsg>Error:" msg "</infomsg>"; exact I : typeclass_instances. +Hint Extern 0 (cfail ?msg) => idtac "Error:" msg; exact I : typeclass_instances. Class cfail2 {T1 T2} (msg1 : T1) (msg2 : T2) := Build_cfail2 : True. -Hint Extern 0 (cfail2 ?msg1 ?msg2) => idtac "<infomsg>Error:" msg1 msg2 "</infomsg>"; exact I : typeclass_instances. +Hint Extern 0 (cfail2 ?msg1 ?msg2) => idtac "Error:" msg1 msg2; exact I : typeclass_instances. Class cfail3 {T1 T2 T3} (msg1 : T1) (msg2 : T2) (msg3 : T3) := Build_cfail3 : True. -Hint Extern 0 (cfail3 ?msg1 ?msg2 ?msg3) => idtac "<infomsg>Error:" msg1 msg2 msg3 "</infomsg>"; exact I : typeclass_instances. +Hint Extern 0 (cfail3 ?msg1 ?msg2 ?msg3) => idtac "Error:" msg1 msg2 msg3; exact I : typeclass_instances. Ltac cidtac msg := constr:(_ : cidtac msg). Ltac cidtac2 msg1 msg2 := constr:(_ : cidtac2 msg1 msg2). @@ -458,9 +457,9 @@ Ltac cfail msg := let dummy := constr:(_ : cfail msg) in constr:(I : I). Ltac cfail2 msg1 msg2 := let dummy := constr:(_ : cfail2 msg1 msg2) in constr:(I : I). Ltac cfail3 msg1 msg2 msg3 := let dummy := constr:(_ : cfail2 msg1 msg2 msg3) in constr:(I : I). -Ltac idtac_goal := lazymatch goal with |- ?G => idtac "<infomsg>Goal:" G "</infomsg>" end. +Ltac idtac_goal := lazymatch goal with |- ?G => idtac "Goal:" G end. Ltac idtac_context := try (repeat match goal with H : _ |- _ => revert H end; idtac_goal; - lazymatch goal with |- ?G => idtac "<infomsg>Context:" G "</infomsg>" end; + lazymatch goal with |- ?G => idtac "Context:" G end; fail). |