From 990de61eb594f86798348c1ff53a8caed2e0e6f2 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 6 Sep 2005 11:59:41 +0000 Subject: [PATCH] Refiner substituted with the type-checker in a case that is known to be already well-typed. --- helm/ocaml/cic_unification/cicRefine.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index df7eca08f..f216b3c5c 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -174,8 +174,10 @@ and type_of_aux' metasenv context t ugraph = | Some (_,C.Def (_,Some ty)) -> t,S.lift n ty,subst,metasenv, ugraph | Some (_,C.Def (bo,None)) -> - let _,ty,subst,metasenv,ugraph = - type_of_aux subst metasenv context (S.lift n bo) ugraph + let ty,ugraph = + (* if it is in the context it must be already well-typed*) + CicTypeChecker.type_of_aux' ~subst metasenv context + (S.lift n bo) ugraph in t,ty,subst,metasenv,ugraph | None -> raise (RefineFailure "Rel to hidden hypothesis") -- 2.39.2