From 9c54f84cee8057fbb90fdfdee1eb7fa9faffbc4f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 21 Feb 2004 21:46:00 +0000
Subject: Correction oubli de report d'une modification de g_vernac (1.69) vers
 g_vernacnew

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

diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index c40cabbd85..c7fdcdc576 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -136,9 +136,9 @@ GEXTEND Gram
   def_token:
     [ [ "Definition" -> (fun _ _ -> ()), (Global, Definition)
       | IDENT "Let" -> (fun _ _ -> ()), (Local, Definition)
-      | IDENT "SubClass"  -> Class.add_subclass_hook, (Global, Coercion)
+      | IDENT "SubClass"  -> Class.add_subclass_hook, (Global, SubClass)
       | IDENT "Local"; IDENT "SubClass"  ->
-          Class.add_subclass_hook, (Local, Coercion) ] ] 
+          Class.add_subclass_hook, (Local, SubClass) ] ] 
   ;
   assumption_token:
     [ [ "Hypothesis" -> (Local, Logical)
-- 
cgit v1.2.3