new ng_library module

[helm.git] / helm / software / components / grafite_parser / grafiteDisambiguate.ml

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index a0558d9f65a06af2f3703d3826f5f4a678339092..b53d6ea3fb6db595178073874e3adc79b89a2416 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -628,11 +628,12 @@ let disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj) =
      match obj with
      | CicNotationPt.Inductive (_,(name,_,_,_)::_)
      | CicNotationPt.Record (_,name,_,_) -> name ^ ".ind"
-     | CicNotationPt.Theorem (_,name,_,_) -> name ^ ".con"
+     | CicNotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
      | CicNotationPt.Inductive _ -> assert false
    in
      UriManager.uri_of_string (baseuri ^ "/" ^ name)
   in
+(*
  let _try_new cic =
   (NCicLibrary.clear_cache ();
    NCicEnvironment.invalidate ();
@@ -721,6 +722,7 @@ let disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj) =
        )
   )
  in 
+*)
 
 
  try
@@ -768,7 +770,7 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
      match obj with
      | CicNotationPt.Inductive (_,(name,_,_,_)::_)
      | CicNotationPt.Record (_,name,_,_) -> name ^ ".ind"
-     | CicNotationPt.Theorem (_,name,_,_) -> name ^ ".con"
+     | CicNotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
      | CicNotationPt.Inductive _ -> assert false
    in
      UriManager.uri_of_string (baseuri ^ "/" ^ name)