From d211f51ea3bf9417422e2bf74ed5dfc1e886ef83 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 29 Jan 2006 16:01:32 +0000
Subject: Ajout syntaxe concrète Proposition, synonyme de Lemma

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7944 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_vernac.ml4 | 1 +
 1 file changed, 1 insertion(+)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 480ce24e73..ad3cc5b363 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -135,6 +135,7 @@ GEXTEND Gram
       | IDENT "Fact" -> Fact
       | IDENT "Remark" -> Remark
       | IDENT "Corollary" -> Corollary
+      | IDENT "Proposition" -> Proposition
       | IDENT "Property" -> Property ] ]
   ;
   def_token:
-- 
cgit v1.2.3