From 5e4bca70bd87a20364ec5867476bbef4912aefdc Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 20 Dec 2000 22:04:41 +0000
Subject: Suppression warning variable de filtrage en majuscule

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1175 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/astterm.ml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 8495df2427..4401848bd3 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -75,8 +75,11 @@ let is_uppercase_var v =
  | _  -> false
 
 let check_uppercase loc ids =
+(* A quoi ça sert ? Pour l'extraction vers ML ? Maintenant elle est externe
   let uplid = List.filter is_uppercase_var ids in
   if uplid <> [] then warning_uppercase loc uplid
+*)
+  ()
 
 (* check that the number of pattern matches the number of matched args *)
 let mssg_number_of_patterns n pl =
-- 
cgit v1.2.3