From f149f4d25c3e65dfca08ee912877f6c8e6c2b00a Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 18 Jun 2010 21:42:56 +0000
Subject: clear/revert dependent: restrict to hyp(h) instead of ident(h)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13169 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Init/Tactics.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 8e1d6d2d8b..a92d9b1eff 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -210,7 +210,7 @@ Tactic Notation "decide" constr(lemma) "with" constr(H) :=
 
 (** Clear an hypothesis and its dependencies *)
 
-Tactic Notation "clear" "dependent" ident(h) :=
+Tactic Notation "clear" "dependent" hyp(h) :=
  let rec depclear h :=
   clear h ||
   match goal with
@@ -222,5 +222,5 @@ Tactic Notation "clear" "dependent" ident(h) :=
 (** Revert an hypothesis and its dependencies :
     this is actually generalize dependent... *)
 
-Tactic Notation "revert" "dependent" ident(h) :=
+Tactic Notation "revert" "dependent" hyp(h) :=
  generalize dependent h.
-- 
cgit v1.2.3