fixed bug in coercion application, input/output swapped in unification

[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 6b5dfca61b829235b852cdc4e7f0a44cd6d52501..b53d6ea3fb6db595178073874e3adc79b89a2416 100644 (file)
--- 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)