Very experimental commit: the type of the source is now required in LetIns

[helm.git] / helm / software / components / acic_content / content2cic.ml

diff --git a/helm/software/components/acic_content/content2cic.ml b/helm/software/components/acic_content/content2cic.ml
index dcec61d84a478018a003a1623227ed8249b79dac..33c5921fba83d99344ad540fb1c96a849caf6fe2 100644 (file)
--- a/helm/software/components/acic_content/content2cic.ml
+++ b/helm/software/components/acic_content/content2cic.ml
@@ -70,17 +70,22 @@ let proof2cic deannotate p =
             | None -> 
                 C.Lambda (C.Anonymous, deannotate h.Con.dec_type, target))
       | `Proof p -> 
+          let ty =
+           match p.Con.proof_conclude.Con.conclude_conclusion with
+              None -> (*Cic.Implicit None*) assert false
+            | Some ty -> deannotate ty
+          in
           (match p.Con.proof_name with
               Some s ->
-                C.LetIn (C.Name s, proof2cic premise_env p, target)
+                C.LetIn (C.Name s, proof2cic premise_env p, ty , target)
             | None -> 
-                C.LetIn (C.Anonymous, proof2cic premise_env p, target)) 
+                C.LetIn (C.Anonymous, proof2cic premise_env p, ty, target)) 
       | `Definition d -> 
            (match d.Con.def_name with
               Some s ->
-                C.LetIn (C.Name s, proof2cic premise_env p, target)
+                C.LetIn (C.Name s, proof2cic premise_env p, deannotate d.Con.def_type, target)
             | None -> 
-                C.LetIn (C.Anonymous, proof2cic premise_env p, target)) 
+                C.LetIn (C.Anonymous, proof2cic premise_env p, deannotate d.Con.def_type, target)) 
       | `Joint {Con.joint_kind = kind; Con.joint_defs = defs} -> 
             (match target with
                C.Rel n ->
@@ -247,14 +252,14 @@ let cobj2obj deannotate (id,params,metasenv,obj) =
                       | _ -> assert false)
                    | Some (`Definition d) ->
                       (match d with
-                          {K.def_name = Some n ; K.def_term = t} ->
-                            Some (Cic.Name n, Cic.Def ((deannotate t),None))
+                          {K.def_name = Some n ; K.def_term = t ; K.def_type = ty} ->
+                            Some (Cic.Name n, Cic.Def (deannotate t,deannotate ty))
                         | _ -> assert false)
                    | Some (`Proof d) ->
                       (match d with
                           {K.proof_name = Some n } ->
                             Some (Cic.Name n,
-                              Cic.Def ((proof2cic deannotate d),None))
+                              Cic.Def ((proof2cic deannotate d),assert false))
                         | _ -> assert false)
                  ) canonical_context
                in