code mort

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3182 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 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 =