From 469a3e2d705d204be699b718d8f818ccd7d01a0c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 15 Nov 2008 17:25:41 +0000 Subject: [PATCH] missing subst added, now apply rule is probably enough to replace apply --- helm/software/components/cic_unification/cicRefine.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index fe5ee7fe3..a263a2eb4 100644 --- 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 -- 2.39.2