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
---
 parsing/g_vernac.ml4 | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 5f656ed5c2..c9fc4e2ffb 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -46,6 +46,7 @@ let noedit_mode = Gram.Entry.create "vernac:noedit_command"
 let class_rawexpr = Gram.Entry.create "vernac:class_rawexpr"
 let thm_token = Gram.Entry.create "vernac:thm_token"
 let def_body = Gram.Entry.create "vernac:def_body"
+let decl_notation = Gram.Entry.create "vernac:decl_notation"
 let typeclass_context = Gram.Entry.create "vernac:typeclass_context"
 let of_type_with_opt_coercion = Gram.Entry.create "vernac:of_type_with_opt_coercion"
 
@@ -119,7 +120,7 @@ let no_coercion loc (c,x) =
 (* Gallina declarations *)
 GEXTEND Gram
   GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion
-    typeclass_context typeclass_constraint;
+    typeclass_context typeclass_constraint decl_notation;
 
   gallina:
       (* Definition, Theorem, Variable, Axiom, ... *)
-- 
cgit v1.2.3