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 3f735a8249f0f23a098d41e18e951e907d351426..d7011c8df4af5c46e8d8dfd4bb3a7cb679757adc 100644 (file)
--- 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 1d0e453b006457909f1bb6a5c55fe33c27c4667e..2f95d663cb8c061686ac02cd5992c0626ff697c0 100644 (file)
--- 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