From adb02ae1008f02dc97564357f0631fe90a944807 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 26 Oct 2002 10:25:07 +0000
Subject: code mort

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3182 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/metasyntax.ml | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index e0206e6f70..66ba77a8a6 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -273,15 +273,6 @@ let make_constr_grammar_rule n fname prod action =
       ]
   }
 
-let rec translate_implicits n = function
-  | [] -> []
-  | q::l when q=n -> true::translate_implicits (n+1) l
-  | impls -> false::translate_implicits (n+1) impls
-
-let implicits_of_extended_reference = function
-  | Libnames.TrueGlobal ref -> translate_implicits 1 (Impargs.implicits_of_global ref)
-  | Libnames.SyntacticDef _ -> []
-
 let create_meta n = "$e"^(string_of_int n)
 
 let strip s =
-- 
cgit v1.2.3