Jason Gross
Jason Gross
> Can't we just fix argosy to make install? What about adding something like ```bash printf '\nMakefile.coq: _CoqProject\n\tcoq_makefile -f _CoqProject -o $@ $(ALL_VFILES)\n' >> Makefile make Makefile.coq make -f Makefile.coq...
> However this clutters the namespace, since if i instead wanted to do `Include F (G X).` having to construct Y leaves the Y name prefixed into all the definitions...
Does `Module M (X : A)
> I started reviewing this, but the change to the indentation made it impossible to see what changed later on in the file, as github got quite confused with the...
> @JasonGross did I get this right? Yes, that sounds right to me
@copilot Do not delete anything in `.` except for `fiat-crypto-build.tar.gz`. But you can delete things in rustup or actions-runner, do more fine-grained printout if you need to ``` === Top...
I want to write an error message that suggests code to insert in the document. Most people don't write code with fully qualified identifiers.
I do ultimately want a message. Going through ident list just seems more flexible for possible future users. I'd be fine with something that just gave me a message though
cc @andres-erbsen