fixed parse error for ocaml 3.08

[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..8d6aed90818268acaae7238b4bf6433576195c4c 100644 (file)
--- a/helm/ocaml/mathql_generator/cGMatchConclusion.ml
+++ b/helm/ocaml/mathql_generator/cGMatchConclusion.ml
@@ -70,10 +70,13 @@ 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
+(*
+        let l' = inspect_uri main l u [] v term in
           inspect_exp_named_subst l' (succ v) exp_named_subst
+*)      
       | Cic.Const (u,exp_named_subst)    ->
          let l' = inspect_uri main l u [] v term in
           inspect_exp_named_subst l' (succ v) exp_named_subst