diff options
Diffstat (limited to 'theories/Program')
| -rw-r--r-- | theories/Program/Equality.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 76dc09b26e..c9ec29d2b0 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -22,7 +22,7 @@ Ltac is_ground_goal := (** Try to find a contradiction. *) -Hint Extern 10 => is_ground_goal ; progress (elimtype False). +Hint Extern 10 => is_ground_goal ; progress exfalso : exfalso. (** We will use the [block] definition to separate the goal from the equalities generated by the tactic. *) |