X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Facic_content%2Facic2content.ml;fp=helm%2Focaml%2Facic_content%2Facic2content.ml;h=ed4eafb4efd2a39774f331cc1b3d6b78ab31da0d;hb=f17da39739c49297bf435896c8cb4e3ac83b95a6;hp=8f3b13cfda82beef7f3ae2bcbc199965ab792b19;hpb=e5cf3788ff8a5416ac13f9d33555ff6f46d89548;p=helm.git diff --git a/helm/ocaml/acic_content/acic2content.ml b/helm/ocaml/acic_content/acic2content.ml index 8f3b13cfd..ed4eafb4e 100644 --- a/helm/ocaml/acic_content/acic2content.ml +++ b/helm/ocaml/acic_content/acic2content.ml @@ -576,7 +576,6 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t = K.ArgProof {body with K.proof_name = name; K.proof_context=context} in List.map2 build_proof patterns name_and_arities in - let teid = get_id te in let context,term = (match build_subproofs_and_args