From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 25 Mar 2008 15:51:59 +0000 (+0000)
Subject: ported to the Cic LetIn with explicit type
X-Git-Tag: make_still_working~5496
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b059fe5ee46d45bc2985b0f46f6a69b4b3be248b;p=helm.git

ported to the Cic LetIn with explicit type
---

diff --git a/helm/software/components/ng_kernel/nCic2OCic.ml b/helm/software/components/ng_kernel/nCic2OCic.ml
index 3f735a824..d7011c8df 100644
--- a/helm/software/components/ng_kernel/nCic2OCic.ml
+++ b/helm/software/components/ng_kernel/nCic2OCic.ml
@@ -12,8 +12,8 @@ let convert_term uri n_fl t =
      Cic.Prod (nn_2_on n,convert_term k s, convert_term (k+1) t)
  | NCic.Lambda  (n,s,t) -> 
      Cic.Lambda(nn_2_on n,convert_term k s, convert_term (k+1) t)
- | NCic.LetIn (n,_,s,t) -> 
-     Cic.LetIn (nn_2_on n,convert_term k s, convert_term (k+1) t)
+ | NCic.LetIn (n,ty_s,s,t) -> 
+     Cic.LetIn (nn_2_on n,convert_term k s,convert_term k ty_s, convert_term (k+1) t)
  | NCic.Sort NCic.Prop -> Cic.Sort Cic.Prop 
  | NCic.Sort NCic.CProp -> Cic.Sort Cic.CProp 
  | NCic.Sort NCic.Set -> Cic.Sort Cic.Set 
diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 1d0e453b0..2f95d663c 100644
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -169,16 +169,13 @@ 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