From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 6 Sep 2004 11:28:23 +0000 (+0000)
Subject: bug in constraint generation for variables fixed
X-Git-Tag: moogle_mathql~13
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cb6e626320bd85ebef29fdb7abbb26dd72c32775;p=helm.git

bug in constraint generation for variables fixed
---

diff --git a/helm/ocaml/mathql_generator/cGMatchConclusion.ml b/helm/ocaml/mathql_generator/cGMatchConclusion.ml
index 42d52a7ac..8d6aed908 100644
--- 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