From 38d436a4b756b95a8a881caf7d1248d49ac4b387 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 18 Nov 2003 10:52:59 +0000
Subject: Code mort

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

diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index c91d1079c5..8ee5c85e09 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -423,16 +423,6 @@ GEXTEND Gram
 	  VernacCoercion (Global, qid, s, t)
 
       (* Implicit *)
-(* Obsolete
-      | IDENT "Syntactic"; IDENT "Definition"; id = IDENT; ":="; c = lconstr;
-         n = OPT [ "|"; n = natural -> n ] ->
-	   let c = match n with
-	     | Some n ->
-		 let l = list_tabulate (fun _ -> (CHole (loc),None)) n in
-		 CApp (loc,c,l)
-	     | None -> c in
-	   VernacNotation (false,c,Some("'"^id^"'",[]),None,None)
-*)
       | IDENT "Implicit"; IDENT "Arguments"; qid = global; 
          pos = OPT [ "["; l = LIST0 ident; "]" -> l ] ->
 	   let pos = option_app (List.map (fun id -> ExplByName id)) pos in
-- 
cgit v1.2.3