From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 5 Sep 2005 16:14:57 +0000 (+0000)
Subject: The refined form of a reference to a let-in bound variable in the context
X-Git-Tag: V_0_1_2_1~94
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8585f72569b06fdc11c881b06b381e68f3ea3094;p=helm.git

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 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")