]> matita.cs.unibo.it Git - helm.git/commitdiff
bug fixed, all convertible was called without a metasenv
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 24 Dec 2008 15:31:20 +0000 (15:31 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 24 Dec 2008 15:31:20 +0000 (15:31 +0000)
helm/software/components/cic_unification/cicRefine.ml

index a2c7707493bb82baafc0561e7f6418a02ea41483..45b2bce8f79b97bdd29e02e795d37cd8e32a549c 100644 (file)
@@ -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)