ng_disambiguation ng_kernel ng_refiner disambiguation: svn:ignore fixed

[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index d9c4608492dc9e02e6d664265ec2bfbfb9628d79..f58f4303c2ada346206ac1fb31c77312581be168 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -560,7 +560,7 @@ let eval_comment status c = status
  * information inside the moo *)
 let add_coercions_of_record_to_moo obj lemmas status =
   let attributes = CicUtil.attributes_of_obj obj in
-  let is_record = function `Class (`Record att) -> Some att | _-> None in
+  let is_record x _ = match x with `Class (`Record att) -> Some att | _-> None in
   match HExtlib.list_findopt is_record attributes with
   | None -> status,[]
   | Some fields ->