From f731cf74872b144b93ad5514ec6fc795f43180de Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 26 Nov 2005 17:38:23 +0000 Subject: [PATCH] Refinement bug fixed. The outtype was not refined if it was an Implicit. --- helm/ocaml/cic_unification/cicRefine.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index f050726bc..239db16cf 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -528,6 +528,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t its instances *) + let outtype,outtypety, subst, metasenv,ugraph4 = + type_of_aux subst metasenv context outtype ugraph4 in (match outtype with | C.Meta (n,l) -> (let candidate,ugraph5,metasenv,subst = @@ -660,9 +662,6 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (Cic.Appl (outtype::right_args@[term']))), subst,metasenv,ugraph) | _ -> (* easy case *) - let outtype,outtypety, subst, metasenv,ugraph4 = - type_of_aux subst metasenv context outtype ugraph4 - in let tlbody_and_type,subst,metasenv,ugraph4 = List.fold_right (fun x (res,subst,metasenv,ugraph) -> -- 2.39.2