X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_generator%2FcGMatchConclusion.ml;fp=helm%2Focaml%2Fmathql_generator%2FcGMatchConclusion.ml;h=42d52a7ac9c6e873fccc950b2b9f28bf6ee93434;hb=e73f439e856f456b47ec6381c0c93594eaac5a82;hp=bb87b461efcf548cb7fe1749043c47d0ca5abc4b;hpb=b2bde540ce5ec2c8731f0353815583bd3d4eba26;p=helm.git

diff --git a/helm/ocaml/mathql_generator/cGMatchConclusion.ml b/helm/ocaml/mathql_generator/cGMatchConclusion.ml
index bb87b461e..42d52a7ac 100644
--- a/helm/ocaml/mathql_generator/cGMatchConclusion.ml
+++ b/helm/ocaml/mathql_generator/cGMatchConclusion.ml
@@ -70,7 +70,7 @@ let levels_of_term metasenv context term =
         Cic.Rel _                        -> l
       | Cic.Meta _                       -> l
       | Cic.Sort _                       -> l 
-      | Cic.Implicit                     -> l 
+      | Cic.Implicit _                   -> l 
       | Cic.Var (u,exp_named_subst)      ->
          let l' = inspect_uri main l u [] v term in
           inspect_exp_named_subst l' (succ v) exp_named_subst