X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicMiniReduction.ml;h=bbf515a99c7908e8898456b7b07b9516f97b47a6;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=cb5875f73c3ef191f18eb5f654eaabebd066910d;hpb=5a92117eeff70048d29e91ba24e113155d956e1b;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicMiniReduction.ml b/helm/ocaml/cic_proof_checking/cicMiniReduction.ml
index cb5875f73..bbf515a99 100644
--- a/helm/ocaml/cic_proof_checking/cicMiniReduction.ml
+++ b/helm/ocaml/cic_proof_checking/cicMiniReduction.ml
@@ -27,22 +27,36 @@ let rec letin_nf =
  let module C = Cic in
   function
      C.Rel _ as t -> t
-   | C.Var _ as t  -> t
+   | C.Var (uri,exp_named_subst) ->
+      let exp_named_subst' =
+       List.map (function (uri,t) -> (uri,letin_nf t)) exp_named_subst
+      in
+       C.Var (uri,exp_named_subst')
    | C.Meta _ as t -> t
    | C.Sort _ as t -> t
-   | C.Implicit as t -> t
+   | C.Implicit _ as t -> t
    | C.Cast (te,ty) -> C.Cast (letin_nf te, letin_nf ty)
    | C.Prod (n,s,t) -> C.Prod (n, letin_nf s, letin_nf t)
    | C.Lambda (n,s,t) -> C.Lambda (n, letin_nf s, letin_nf t)
    | C.LetIn (n,s,t) -> CicSubstitution.subst (letin_nf s) t
    | C.Appl l -> C.Appl (List.map letin_nf l)
-   | C.Const _ as t -> t
-   | C.Abst _ as t -> t
-   | C.MutInd _ as t -> t
-   | C.MutConstruct _ as t -> t
-   | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
-      C.MutCase (sp,cookingsno,i,letin_nf outt, letin_nf t,
-       List.map letin_nf pl)
+   | C.Const (uri,exp_named_subst) ->
+      let exp_named_subst' =
+       List.map (function (uri,t) -> (uri,letin_nf t)) exp_named_subst
+      in
+       C.Const (uri,exp_named_subst')
+   | C.MutInd (uri,typeno,exp_named_subst) ->
+      let exp_named_subst' =
+       List.map (function (uri,t) -> (uri,letin_nf t)) exp_named_subst
+      in
+       C.MutInd (uri,typeno,exp_named_subst')
+   | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
+      let exp_named_subst' =
+       List.map (function (uri,t) -> (uri,letin_nf t)) exp_named_subst
+      in
+       C.MutConstruct (uri,typeno,consno,exp_named_subst')
+   | C.MutCase (sp,i,outt,t,pl) ->
+      C.MutCase (sp,i,letin_nf outt, letin_nf t, List.map letin_nf pl)
    | C.Fix (i,fl) ->
       let substitutedfl =
        List.map