bug in constraint generation for variables fixed

[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 42d52a7ac9c6e873fccc950b2b9f28bf6ee93434..8d6aed90818268acaae7238b4bf6433576195c4c 100644 (file)
--- a/helm/ocaml/mathql_generator/cGMatchConclusion.ml
+++ b/helm/ocaml/mathql_generator/cGMatchConclusion.ml
@@ -72,8 +72,11 @@ let levels_of_term metasenv context term =
       | Cic.Sort _                       -> 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