From: Claudio Sacerdoti Coen Date: Thu, 31 May 2007 15:02:52 +0000 (+0000) Subject: Bug fixed: wrong id. X-Git-Tag: 0.4.95@7852~417 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f768cb971f7a9dcdb130c1ce29be58eb4d083d95;p=helm.git Bug fixed: wrong id. --- diff --git a/components/acic_content/acic2content.ml b/components/acic_content/acic2content.ml index a2e7622ea..1b8c287fa 100644 --- a/components/acic_content/acic2content.ml +++ b/components/acic_content/acic2content.ml @@ -494,7 +494,7 @@ 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; }