X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2Facic2content.ml;h=eddee38b1a51ed2c985df789006c574ae21604e0;hb=55ec3926f6fbb5dba13705659fe94d0db38b2666;hp=1b8c287fabef5f77c261974cc9d84c07a4703635;hpb=cebed8851dcaf8ceeb4e5f74b52705bf0c18a456;p=helm.git

diff --git a/helm/software/components/acic_content/acic2content.ml b/helm/software/components/acic_content/acic2content.ml
index 1b8c287fa..eddee38b1 100644
--- a/helm/software/components/acic_content/acic2content.ml
+++ b/helm/software/components/acic_content/acic2content.ml
@@ -479,7 +479,8 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
             }
           in
           generate_intros_let_tac seed id n s true proof'' name ~ids_to_inner_types
-        else raise Not_a_proof 
+        else 
+          raise Not_a_proof 
     | C.ALetIn (id,n,s,t) ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
         if sort = `Prop then
@@ -500,7 +501,8 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
             }
           in
           generate_intros_let_tac seed id n s false proof'' name ~ids_to_inner_types
-        else raise Not_a_proof 
+        else 
+          raise Not_a_proof
     | C.AAppl (id,li) ->
         (try coercion 
            seed li ~ids_to_inner_types ~ids_to_inner_sorts