X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=b53d6ea3fb6db595178073874e3adc79b89a2416;hb=7d9753115cb26bf27a739e9e1d753fd60b185c17;hp=6b5dfca61b829235b852cdc4e7f0a44cd6d52501;hpb=7477c3dbbc2fafe248d48302be0d6ba4cb38d062;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 6b5dfca61..b53d6ea3f 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -628,7 +628,7 @@ 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)
@@ -770,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)