From 32e4b999885f34e89077c5a4d686f75b9633ad87 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 23 Nov 2000 13:27:04 +0000
Subject: Bug qualidconstarg (intervient pour Transparent)

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

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index bcbb32d5bc..39bdda79bd 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -55,7 +55,7 @@ GEXTEND Gram
     [ [ l = LIST1 qualidarg -> l ] ]
   ;
   ne_qualidconstarg_list:
-    [ [ l = LIST1 qualidarg -> l ] ]
+    [ [ l = LIST1 qualidconstarg -> l ] ]
   ;
   ne_num_list:
     [ [ n = numarg; l = ne_num_list -> n :: l | n = numarg -> [n] ] ]
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index b72aa80e1f..6363decfe1 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -488,8 +488,7 @@ let _ =
     (fun id_list () ->
        List.iter 
 	 (function 
-(*	    | VARG_CONSTANT sp -> Global.set_transparent sp *)
-	    | VARG_QUALID sp -> Global.set_transparent sp
+	    | VARG_CONSTANT sp -> Global.set_transparent sp
 	    |   _  -> bad_vernac_args "TRANSPARENT")
 	 id_list)
     
-- 
cgit v1.2.3