Require Import FixedPoint ClassicalDescription. Extract Constant fixp => "let rec t d f x = f (fun y -> t d f y) x in t". Extract Constant constructive_definite_description => "Obj.magic".