missing subst added, now apply rule is probably enough to replace apply

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index fe5ee7fe378942f14c08ebe923a7a689698af4b4..a263a2eb4dc4fcece602edd7dfc1916f062ca9d6 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -406,7 +406,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
               type_of_aux subst' metasenv' context te ugraph1
             in
             let rec count_prods context ty =
-              match CicReduction.whd context ty with
+              match CicReduction.whd context ~subst:subst'' ty with
               | Cic.Prod (n,s,t) -> 
                  1 + count_prods (Some (n,Cic.Decl s)::context) t
               | _ -> 0
@@ -417,7 +417,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                let rec aux t m s ug it = function
                  | 0 -> t,it,m,s,ug
                  | n ->
-                      match CicReduction.whd context it with
+                      match CicReduction.whd context ~subst:s it with
                       | Cic.Prod (_,src,tgt) -> 
                           let newmeta, metaty, s, m, ug =
                             type_of_aux s m context (Cic.Implicit None) ug
@@ -425,7 +425,6 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                           let s,m,ug = 
                             fo_unif_subst s context m metaty src ug
                           in
-(*                           prerr_endline "saturo"; *)
                           let t =
                             match t with
                             | Cic.Appl l -> Cic.Appl (l @ [newmeta])
@@ -437,7 +436,6 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                  aux te' metasenv'' subst'' ugraph2 inferredty
                    (max 0 (inf_prods - exp_prods))
             in
-(*             prerr_endline ("ottengo: " ^ CicPp.ppterm te'); *)
             let (te', ty'), subst''',metasenv''',ugraph3 =
               coerce_to_something true localization_tbl te' inferredty ty'
                 subst'' metasenv'' context ugraph2