- patched for new CIC

[helm.git] / helm / ocaml / mathql_generator / cGMatchConclusion.ml

diff --git a/helm/ocaml/mathql_generator/cGMatchConclusion.ml b/helm/ocaml/mathql_generator/cGMatchConclusion.ml
index bb87b461efcf548cb7fe1749043c47d0ca5abc4b..42d52a7ac9c6e873fccc950b2b9f28bf6ee93434 100644 (file)
--- 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