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.

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 148450f5d17f1375b275186f3c08d807d0780a6b..df7eca08f398f35141d021091d254c0a7408ba88 100644 (file)
--- 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")