X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FoCic2NCic.ml;h=b2591b361c2ba7c5d9f6030ea85a9f7630f55598;hb=402eeb8676ba04d5e7e653561c9dd332a0c8a078;hp=0d00f031f18c558cbba117337fe7bda33ca8c440;hpb=bd5488c8eaa88e27d6e9e6c46566f1ed8f1a59b0;p=helm.git

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 0d00f031f..b2591b361 100644
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -46,17 +46,19 @@ let splat_args_for_rel ctx t =
 
 let splat_args ctx t n_fix = 
   let bound, free, primo_ce_dopo_fix = context_tassonomy ctx in
-  let rec aux = function
-    | 0 -> []
-    | n -> 
-       (match List.nth ctx (n-1) with
-        | Ce _ when n <= bound -> NCic.Rel n
-        | Fix (refe, _, _) when n < primo_ce_dopo_fix ->
-           splat_args_for_rel ctx (NCic.Const refe)
-        | Fix _ | Ce _ -> NCic.Rel (n - n_fix)
-       ) :: aux (n-1)
-  in
-  NCic.Appl (t:: aux (List.length ctx))
+  if ctx = [] then t
+  else
+   let rec aux = function
+     | 0 -> []
+     | n -> 
+        (match List.nth ctx (n-1) with
+         | Ce _ when n <= bound -> NCic.Rel n
+         | Fix (refe, _, _) when n < primo_ce_dopo_fix ->
+            splat_args_for_rel ctx (NCic.Const refe)
+         | Fix _ | Ce _ -> NCic.Rel (n - n_fix)
+        ) :: aux (n-1)
+   in
+   NCic.Appl (t:: aux (List.length ctx))
 ;;
 
 (* we are lambda-lifting also variables that do not occur *)
@@ -75,7 +77,7 @@ let convert_term uri t =
             (fun (name,ty,_) (ctx, fixpoints, tys, idx) -> 
               let ty, fixpoints_ty = aux octx ctx n_fix uri ty in
               let r = NReference.reference_of_ouri buri(NReference.CoFix idx) in
-              ctx @ [Fix (r,name,ty)], fixpoints_ty @ fixpoints,ty::tys,idx+1)
+              Fix (r,name,ty) :: ctx, fixpoints_ty @ fixpoints,ty::tys,idx+1)
             fl ([], [], [], 0)
         in
         let bctx = bctx @ ctx in
@@ -117,7 +119,7 @@ let convert_term uri t =
               let r = 
                 NReference.reference_of_ouri buri (NReference.Fix (idx,recno)) 
               in
-              ctx @ [Fix (r,name,ty)], fixpoints_ty@fixpoints,ty::tys,idx+1)
+              Fix (r,name,ty) :: ctx, fixpoints_ty@fixpoints,ty::tys,idx+1)
             fl ([], [], [], 0)
         in
         let bctx = bctx @ ctx in
@@ -167,25 +169,22 @@ let convert_term uri t =
         let octx = Some (name, Cic.Decl old_s) :: octx in
         let t, fixpoints_t = aux octx ctx n_fix uri t in
         NCic.Prod (cn_to_s name, s, t), fixpoints_s @ fixpoints_t
-    | Cic.LetIn (name, (s as old_s), t) ->
-        let s, fixpoints_s = aux octx ctx n_fix uri s in
-        let old_ty,_ = 
-          CicTypeChecker.type_of_aux' [] octx old_s CicUniv.oblivion_ugraph 
-        in
-        let ty, fixpoints_ty = aux octx ctx n_fix uri old_ty in
-        let ctx = Ce (cn_to_s name, NCic.Def (s, ty)) :: ctx in
-        let octx = Some (name, Cic.Def (old_s, Some old_ty)) :: octx in
+    | Cic.LetIn (name, (te as old_te), (ty as old_ty), t) ->
+        let te, fixpoints_s = aux octx ctx n_fix uri te in
+        let ty, fixpoints_ty = aux octx ctx n_fix uri ty in
+        let ctx = Ce (cn_to_s name, NCic.Def (te, ty)) :: ctx in
+        let octx = Some (name, Cic.Def (old_te, old_ty)) :: octx in
         let t, fixpoints_t = aux octx ctx n_fix uri t in
-        NCic.LetIn (cn_to_s name, ty, s, t), 
+        NCic.LetIn (cn_to_s name, ty, te, t), 
         fixpoints_s @ fixpoints_t @ fixpoints_ty
     | Cic.Cast (t,ty) ->
         let t, fixpoints_t = aux octx ctx n_fix uri t in
         let ty, fixpoints_ty = aux octx ctx n_fix uri ty in
         NCic.LetIn ("cast", ty, t, NCic.Rel 1), fixpoints_t @ fixpoints_ty
     | Cic.Sort Cic.Prop -> NCic.Sort NCic.Prop,[]
-    | Cic.Sort Cic.Set -> NCic.Sort NCic.Set,[]
     | Cic.Sort Cic.CProp -> NCic.Sort NCic.CProp,[]
     | Cic.Sort (Cic.Type _) -> NCic.Sort (NCic.Type 0),[] 
+    | Cic.Sort Cic.Set -> NCic.Sort (NCic.Type 0),[] 
        (* calculate depth in the univ_graph*)
     | Cic.Appl l -> 
         let l, fixpoints =