(* -*- coq-prog-args: ("-w" "-native-compiler-disabled" "-native-compiler" "ondemand"); -*- *)