many changes:

[helm.git] / components / cic / deannotate.ml

diff --git a/components/cic/deannotate.ml b/components/cic/deannotate.ml
index f04f5aa10e1197ea61c8338e3a39a01968083346..b7c7d1113cdbd6fea17bb96ad90742b21436b3bc 100644 (file)
--- 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) ->