X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Fcic%2Fdeannotate.ml;h=b7c7d1113cdbd6fea17bb96ad90742b21436b3bc;hb=e016b4d32f05113a882e83a9fc8319751224c975;hp=f04f5aa10e1197ea61c8338e3a39a01968083346;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/cic/deannotate.ml b/components/cic/deannotate.ml
index f04f5aa10..b7c7d1113 100644
--- a/components/cic/deannotate.ml
+++ b/components/cic/deannotate.ml
@@ -89,6 +89,22 @@ let deannotate_inductiveType (_, name, isinductive, arity, cons) =
   List.map (fun (id,ty) -> (id,deannotate_term ty)) cons)
 ;;
 
+let deannotate_conjectures =
+ let module C = Cic in
+  List.map
+   (function 
+     (_,id,acontext,con) -> 
+      let context = 
+       List.map 
+        (function 
+          | _,Some (n,(C.ADef at)) -> Some(n,(C.Def((deannotate_term at),None)))
+          | _,Some (n,(C.ADecl at)) -> Some (n,(C.Decl (deannotate_term at)))
+          | _,None -> None)
+        acontext  
+      in
+       (id,context,deannotate_term con))
+;;
+
 let deannotate_obj =
  let module C = Cic in
   function
@@ -103,21 +119,7 @@ let deannotate_obj =
    | C.ACurrentProof (_, _, name, conjs, bo, ty, params, attrs) ->
       C.CurrentProof (
        name,
-        List.map
-         (function 
-           (_,id,acontext,con) -> 
-	    let context = 
-	     List.map 
-	      (function 
-	          _,Some (n,(C.ADef at)) ->
-                   Some (n,(C.Def ((deannotate_term at),None)))
-	        | _,Some (n,(C.ADecl at)) ->
-                   Some (n,(C.Decl (deannotate_term at)))
-	        | _,None -> None
-              ) acontext  
-            in
-	     (id,context,deannotate_term con) 
-         ) conjs,
+       deannotate_conjectures conjs,
        deannotate_term bo,deannotate_term ty, params, attrs
       )
    | C.AInductiveDefinition (_, tys, params, parno, attrs) ->