]> matita.cs.unibo.it Git - helm.git/commitdiff
Refiner substituted with the type-checker in a case that is known to be already
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 6 Sep 2005 11:59:41 +0000 (11:59 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 6 Sep 2005 11:59:41 +0000 (11:59 +0000)
well-typed.

helm/ocaml/cic_unification/cicRefine.ml

index df7eca08f398f35141d021091d254c0a7408ba88..f216b3c5c03429324561f49e8a89e770246063e1 100644 (file)
@@ -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")