X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fcontent2pres.ml;fp=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fcontent2pres.ml;h=fc3a47b5e1c564fb168e1fcba94b09ccd40fa86e;hb=1b70a1f66be53f76e475383e86d63c2b5c1fbcaa;hp=4d5ec86f5aff02446e9d0b6d44c6278b48991039;hpb=f49690e1d1b39ccad40f1e874d9d19f6ffc289e0;p=helm.git diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml index 4d5ec86f5..fc3a47b5e 100644 --- a/helm/software/components/content_pres/content2pres.ml +++ b/helm/software/components/content_pres/content2pres.ml @@ -183,7 +183,7 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = in context2pres (match skip_initial_lambdas_internal with - Some (`Now n) -> snd (HExtlib.split_nth "CP 1" n p.Con.proof_context) + Some (`Now n) -> snd (HExtlib.split_nth n p.Con.proof_context) | _ -> p.Con.proof_context) presacontext in