From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 24 Dec 2008 15:31:20 +0000 (+0000)
Subject: bug fixed, all convertible was called without a metasenv
X-Git-Tag: make_still_working~4327
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9dee1479d1d4ee35e9768612b35741e2ecde8fc0;hp=6e75e2415b0433a134e0050d63d627a66efea7a4;p=helm.git

bug fixed, all convertible was called without a metasenv
---

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index a2c770749..45b2bce8f 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1451,7 +1451,8 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                   fo_unif_subst subst context metasenv newhety expty ugraph
                 in
                 let b, ugraph =
-                  CicReduction.are_convertible ~subst context infty expty ugraph
+                  CicReduction.are_convertible 
+                    ~subst ~metasenv context infty expty ugraph
                 in
                 if b then 
                   Some ((t,infty), subst, metasenv, ugraph)