From 8585f72569b06fdc11c881b06b381e68f3ea3094 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 5 Sep 2005 16:14:57 +0000 Subject: [PATCH] The refined form of a reference to a let-in bound variable in the context used to be the zeta-expanded form. It is now the reference. --- helm/ocaml/cic_unification/cicRefine.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 148450f5d..df7eca08f 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -174,7 +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)) -> - type_of_aux subst metasenv context (S.lift n bo) ugraph + let _,ty,subst,metasenv,ugraph = + type_of_aux subst metasenv context (S.lift n bo) ugraph + in + t,ty,subst,metasenv,ugraph | None -> raise (RefineFailure "Rel to hidden hypothesis") with _ -> raise (RefineFailure "Not a close term") -- 2.39.2