camlp5 IFNDEF STRICT doing the opposite of what I expect

Question

HOL Light has some tortured camlp5 logic to change the syntax of ocaml. I've patched it to work under ocaml 4.04 and 6.17, but it only works under camlp5 strict mode. I've traced the problem to the following code:

value vala_map f =
  IFNDEF STRICT THEN
    fun x -> f x
  ELSE
    fun
    [ Ploc.VaAnt s -> Ploc.VaAnt s
    | Ploc.VaVal x -> Ploc.VaVal (f x) ]
  END
;

To the best of my understanding, this should execute the second macro branch if STRICT is defined, and the first if STRICT is not defined. I've checked with camlp5r pa_macro.cmo -defined that STRICT is defined on my machine with camlp5 strict mode, and undefined on my machine with camlp5 transitional mode.

Unfortunately, the second branch is taken on both machines, as if STRICT was defined on both. Changing IFNDEF STRICT THEN to IFNDEF BLAH THEN switches to the first branch, again as if STRICT was defined on both. However, putting an UNDEF STRICT; immediately before the code has no effect.

I'm at a loss, and would love any suggestions for what might be happening, or experiments to run next.

Answer 1

Mystery solved: one of the modules imported by that file explicitly turns on strict mode. The UNDEF had no effect because STRICT is apparently a specially handled builtin.