From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
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