From: Claudio Sacerdoti Coen Date: Tue, 6 Sep 2005 08:43:30 +0000 (+0000) Subject: Serious bug fixed: unsharing was not performed over sequents. X-Git-Tag: V_0_1_2_1~87 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fac7b34e0f5b78a627c45115e7e35addcd9ae278;p=helm.git Serious bug fixed: unsharing was not performed over sequents. --- diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml index 9c62ae845..210f3ed2f 100644 --- a/helm/ocaml/cic_omdoc/cic2acic.ml +++ b/helm/ocaml/cic_omdoc/cic2acic.ml @@ -415,6 +415,27 @@ let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) = let ids_to_hypotheses = Hashtbl.create 23 in let hypotheses_seed = ref 0 in let seed = ref 1 in (* 'i0' is used for the whole sequent *) + let sequent = + let i,canonical_context,term = sequent in + let canonical_context' = + List.fold_right + (fun d canonical_context' -> + let d' = + match d with + None -> None + | Some (n, Cic.Decl t)-> + 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 + in + d::canonical_context' + ) [] canonical_context + in + let term' = Unshare.unshare term in + (i,canonical_context',term') + in let (metano,acontext,agoal) = aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids ids_to_inner_sorts ids_to_inner_types ids_to_hypotheses hypotheses_seed