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

[helm.git] / helm / software / components / disambiguation / disambiguate.ml

diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml
index 354a737832bd15085e5ce8f89ec6f8fa25951cd0..52411d6ed2abf458ef8706691419713ffb6eb6bc 100644 (file)
--- a/helm/software/components/disambiguation/disambiguate.ml
+++ b/helm/software/components/disambiguation/disambiguate.ml
@@ -334,7 +334,7 @@ let domain_of_term ~context term =
 let domain_of_obj ~context ast =
  assert (context = []);
   match ast with
-   | Ast.Theorem (_,_,ty,bo) ->
+   | Ast.Theorem (_,_,ty,bo,_) ->
       domain_of_term [] ty
       @ (match bo with
           None -> []