From 8f4a6940a523c116343f345733901e57bb2649a8 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 24 Nov 2009 23:05:14 +0000
Subject: Minor fixes in typeclasses, avoiding repeated evar normalizations.
 Improve generalization by equalities tactic, now allowing to generalize an
 arbitrary application, e.g. in preparation for applying an elimination
 principle for a function. This adds a flag to generalize_dep so that it
 doesn't abstract the variable if it is defined, just introducing a let-in.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12541 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Program/Equality.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories/Program')

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. *)
-- 
cgit v1.2.3