I do not know why, but

[helm.git] / helm / software / components / acic_content / acic2content.ml

diff --git a/helm/software/components/acic_content/acic2content.ml b/helm/software/components/acic_content/acic2content.ml
index 23d6447863a9f9335f101d240e1edfa51ca885dd..eddee38b1a51ed2c985df789006c574ae21604e0 100644 (file)
--- 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
@@ -494,13 +495,14 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
             { proof' with
                K.proof_name = None;
                K.proof_context = 
-                 ((build_def_item seed id n s ids_to_inner_sorts 
+                 ((build_def_item seed (get_id s) n s ids_to_inner_sorts 
                    ids_to_inner_types):> Cic.annterm K.in_proof_context_element)
                  ::proof'.K.proof_context;
             }
           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
@@ -805,7 +807,7 @@ and coercion seed li ~ids_to_inner_types ~ids_to_inner_sorts =
     | ((Cic.AConst _) as he)::tl
     | ((Cic.AMutInd _) as he)::tl
     | ((Cic.AMutConstruct _) as he)::tl when 
-       CoercGraph.is_a_coercion (Deannotate.deannotate_term he) &&
+       CoercDb.is_a_coercion' (Deannotate.deannotate_term he) &&
        !hide_coercions ->
         let rec last =
          function