From 93ac7bd0475563be89d978d82a7579bfdcf2b494 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 7 Nov 2005 18:44:56 +0000 Subject: [PATCH] Let-ins with types can be produced. --- helm/ocaml/cic_omdoc/cic2acic.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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 [] -- 2.39.2