X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicSubstitution.ml;h=8d1dad9e2c2af09ccded670260c3b9c0b8971927;hb=9f66cc89caf70d20a0e4c0d55796da6082d60976;hp=a4340583efc8b1f98cbacfdb58a7f94efa8249a9;hpb=4e3d7b4b47f66f0745333bfd4efcb27b4528f4c3;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicSubstitution.ml b/helm/software/components/cic_proof_checking/cicSubstitution.ml
index a4340583e..8d1dad9e2 100644
--- a/helm/software/components/cic_proof_checking/cicSubstitution.ml
+++ b/helm/software/components/cic_proof_checking/cicSubstitution.ml
@@ -62,7 +62,8 @@ let lift_from k n =
     | C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty)
     | C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t)
     | C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t)
-    | C.LetIn (n,s,t) -> C.LetIn (n, liftaux k s, liftaux (k+1) t)
+    | C.LetIn (n,s,ty,t) ->
+       C.LetIn (n, liftaux k s, liftaux k ty, liftaux (k+1) t)
     | C.Appl l -> C.Appl (List.map (liftaux k) l)
     | C.Const (uri,exp_named_subst) ->
        let exp_named_subst' = 
@@ -142,7 +143,8 @@ let rec subst ?(avoid_beta_redexes=false) arg =
     | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
     | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
     | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
-    | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t)
+    | C.LetIn (n,s,ty,t) ->
+       C.LetIn (n, substaux k s, substaux k ty, substaux (k + 1) t)
     | C.Appl (he::tl) ->
        (* Invariant: no Appl applied to another Appl *)
        let tl' = List.map (substaux k) tl in
@@ -257,7 +259,8 @@ debug_print (lazy "---- END\n\n ") ;
     | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
     | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
     | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
-    | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t)
+    | C.LetIn (n,s,ty,t) ->
+       C.LetIn (n, substaux k s, substaux k ty, substaux (k + 1) t)
     | C.Appl (he::tl) ->
        (* Invariant: no Appl applied to another Appl *)
        let tl' = List.map (substaux k) tl in
@@ -398,7 +401,7 @@ let subst_meta l t =
     | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) (*CSC ??? *)
     | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k + 1) t)
     | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k + 1) t)
-    | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k + 1) t)
+    | C.LetIn (n,s,ty,t) -> C.LetIn (n, aux k s, aux k ty, aux (k + 1) t)
     | C.Appl l -> C.Appl (List.map (aux k) l)
     | C.Const (uri,exp_named_subst) ->
        let exp_named_subst' =
@@ -437,3 +440,4 @@ let subst_meta l t =
   aux 0 t          
 ;;
 
+Deannotate.lift := lift;;