X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Focaml%2Fcic_omdoc%2Fcic2acic.ml;h=210f3ed2f94fce78cabafea90cbfc825906c271a;hb=52af0e3a6ab827464f33b90bf0d39e5df3169499;hp=9c62ae845acece068ea1e78362fef7b1e5eafe9b;hpb=4c61dbec2286f7a39a88c30d657947b2b144ca4a;p=helm.git

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