From 49356f9dd870d7d42e1e4ffbfc00906832197ef1 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sun, 9 Nov 2003 15:16:46 +0000
Subject: Traduction semantique des InHyp de clause en InHypValue si local def

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4841 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_tactic.ml4 | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'parsing/g_tactic.ml4')

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 74352c0bb..491fd467f 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -217,8 +217,9 @@ GEXTEND Gram
       | s = IDENT; c = constr -> ExtraRedExpr (s,c) ] ]
   ;
   hypident:
-    [ [ id = id_or_meta -> InHyp id
-      | "("; "Type"; "of"; id = id_or_meta; ")" -> InHypType id ] ]
+    [ [ id = id_or_meta -> id,(InHyp,ref None)
+      | "("; "Type"; "of"; id = id_or_meta; ")" -> id,(InHypTypeOnly,ref None)
+    ] ]
   ;
   clause:
     [ [ "in"; idl = LIST1 hypident -> idl
-- 
cgit v1.2.3