From 4da5cd28c6080ceeb66acc2163cf10a43e8bcade Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 3 Sep 2008 00:03:32 +0000
Subject: Correct handling of implicit arguments in [Equations] definitions,
 support for "where" notation declarations as well. Better checking of
 recursivity or not, after type-checking.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11354 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 869df369b8..2bf25c8e70 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -389,7 +389,7 @@ Ltac depelim id :=
    (used internally). *)
 
 Ltac destruct_last :=
-  on_last_hyp ltac:(fun id => generalize_eqs id ; destruct id).
+  on_last_hyp ltac:(fun id => simpl in id ; generalize_eqs id ; destruct id).
 
 (** The rest is support tactics for the [Equations] command. *)
 
-- 
cgit v1.2.3