From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 7 Nov 2005 18:44:56 +0000 (+0000)
Subject: Let-ins with types can be produced.
X-Git-Tag: V_0_7_2_3~114
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=93ac7bd0475563be89d978d82a7579bfdcf2b494;p=helm.git

Let-ins with types can be produced.
---

diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml
index 0d3127c31..4c7b955c9 100644
--- a/helm/ocaml/cic_omdoc/cic2acic.ml
+++ b/helm/ocaml/cic_omdoc/cic2acic.ml
@@ -382,7 +382,7 @@ let aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids
            Hashtbl.add ids_to_hypotheses hid binding ;
            incr hypotheses_seed ;
            match binding with
-               Some (n,Cic.Def (t,None)) ->
+               Some (n,Cic.Def (t,_)) ->
                  let acic = acic_of_cic_context context idrefs t None in
                  (binding::context),
                    ((hid,Some (n,Cic.ADef acic))::acontext),(hid::idrefs)
@@ -393,7 +393,6 @@ let aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids
              | None ->
                  (* Invariant: "" is never looked up *)
                   (None::context),((hid,None)::acontext),""::idrefs
-             | Some (_,Cic.Def (_,Some _)) -> assert false
          ) context ([],[],[])
        )
   in 
@@ -421,7 +420,8 @@ let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) =
                Some (n, Cic.Decl (Unshare.unshare t))
             | Some (n, Cic.Def (t,None)) ->
                Some (n, Cic.Def ((Unshare.unshare t),None))
-            | Some (_,Cic.Def (_,Some _)) -> assert false
+            | Some (n,Cic.Def (bo,Some ty)) ->
+               Some (n, Cic.Def (Unshare.unshare bo,Some (Unshare.unshare ty)))
           in
            d::canonical_context'
         ) canonical_context []