From 44696bb5b16f60cefe6d133f6388fd84bcea369f Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 9 Feb 2016 16:28:48 -0500 Subject: [PATCH] Beef up [equality] --- Frap.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Frap.v b/Frap.v index 94e7211..a49b116 100644 --- a/Frap.v +++ b/Frap.v @@ -62,7 +62,7 @@ Ltac linear_arithmetic := intros; rewrite Heq in *; clear Heq end; omega. -Ltac equality := congruence. +Ltac equality := intuition congruence. Ltac cases E := ((is_var E; destruct E)