Cic.term and Cic.obj unused!

[helm.git] / matita / components / lexicon / lexiconSync.ml

diff --git a/matita/components/lexicon/lexiconSync.ml b/matita/components/lexicon/lexiconSync.ml
index 325a8d8375ac392cfea04c1de76ac324b3c7dca8..33d21a93fa256dde60139579db8070f15a362982 100644 (file)
--- a/matita/components/lexicon/lexiconSync.ml
+++ b/matita/components/lexicon/lexiconSync.ml
@@ -73,14 +73,6 @@ let add_alias_for_constant status uri =
  let new_env = build_aliases [(name,uri)] in
  LexiconEngine.set_proof_aliases status new_env
 
-let add_aliases_for_object status uri =
- function
-    Cic.InductiveDefinition (types,_,_,_) ->
-     add_aliases_for_inductive_def status types uri
-  | Cic.Constant _ -> add_alias_for_constant status uri
-  | Cic.Variable _
-  | Cic.CurrentProof _ -> assert false
-  
 let add_aliases_for_objs status =
   function
    `Old _ -> assert false (* MATITA 1.0 *)