sci-mathematics/coq-8.3 has a patch for that which is included in sci-mathematics/coq-8.3_p1. It uses 'IFDEF CAMLP5_6_00 THEN ... ELSE ... END' to make it compatible with both dev-ml/camlp5-5 and dev-ml/camlp5-6. We need something similar for sci-mathematics/coq-8.2_p1 and sci-mathematics/coq-8.2_p2.
Created attachment 262823 [details, diff] sci-mathematics/coq/files/coq-8.2_p2-camlp5-6-compat.patch Here is a patch I made for sci-mathematics/coq-8.2_p2 that should be ok with both dev-ml/camlp5-5 and dev-ml/camlp5-6.
Is there a good reason to stay on 8.2 instead of moving on? I will request stable for 8.3_p1 to resolve this. Please scream if you need 8.2 for a good reason. (Current stable is broken with newer versions of make)
Well, there are some incompatibilities between 8.2 and 8.3 (see http://coq.inria.fr/V8.3/COMPATIBILITY). I've encountered several programs that rely on coq and have still to be ported to 8.3 (the "-compat 8.2" option is far from being perfect). coq-8.2_p2 already has a make-3.82 compatibility patch. So even if you stabilize coq-8.3_p1, I would not mind if you could add my patch for coq-8.2_p2 and only drop coq-8.2_p1. But if that's really a bother I can keep it on my local overlay for the time being.
Agreed. I applied your patch to 8.2_p2. Thanks for the effort. + 20 Feb 2011; Thomas Kahle <tomka@gentoo.org> coq-8.2_p2.ebuild, + +files/coq-8.2_p2-camlp5-6-compat.patch: + Added camlp5-6 support to the 8.2 branch (bug 355297), patch by + Jonathan-Christofer Demay +
