X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=b535b9ebe987677505d7d9b40a2c59731a4c2606;hb=c22f39a5d5afc0ef55beb221e00e2e6703b13d90;hp=40eaa1ba6351533ce31173749f6b4c5f1ccece7a;hpb=24898ae10160660dac8d13fda33d90d3b1f4ace6;p=helm.git

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 40eaa1ba6..b535b9ebe 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -337,8 +337,8 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt
              | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
       | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
 
-and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
-     ugraph
+and type_of_aux' ?(clean_dummy_dependent_types=true) 
+  ?(localization_tbl = Cic.CicHash.create 1) metasenv subst context t ugraph
 =
   let rec type_of_aux subst metasenv context t ugraph =
     let module C = Cic in
@@ -1828,7 +1828,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
   (* eat prods ends here! *)
   
   let t',ty,subst',metasenv',ugraph1 =
-   type_of_aux [] metasenv context t ugraph
+   type_of_aux subst metasenv context t ugraph
   in
   let substituted_t = CicMetaSubst.apply_subst subst' t' in
   let substituted_ty = CicMetaSubst.apply_subst subst' ty in
@@ -1872,7 +1872,21 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
    else
     substituted_metasenv
   in
-    (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1) 
+    (cleaned_t,cleaned_ty,cleaned_metasenv,subst',ugraph1) 
+;;
+
+let type_of metasenv subst context t ug =
+  type_of_aux' metasenv subst context t ug
+;;
+
+let type_of_aux' 
+  ?clean_dummy_dependent_types ?localization_tbl metasenv context t ug
+=
+  let t,ty,m,s,ug = 
+    type_of_aux' ?clean_dummy_dependent_types ?localization_tbl 
+      metasenv [] context t ug
+  in
+  t,ty,m,ug
 ;;
 
 let undebrujin uri typesno tys t =