master

GGaëtan GilbertMove print-mod-uid to main rocq exe instead of rocq repl

4dbebe6d创建于 20 天前历史提交

文件	最后提交记录	最后更新时间
rocqide	Move print-mod-uid to main rocq exe instead of rocq repl This avoids having to deal with random initializations, needing -q, and whatever else rocq repl involves. AFAICT -print-mod-uid is an internal flag used only by rocq makefile (for installing native files). rocq makefile does not support -native-output-dir AFAICT so we hardcode .coq-native.	20 天前