master

PPierre RouxMake `f (x:=e)%s` parse as `f (x:=e%s)` instead of `(f (x:=e))%s`

d597975f创建于 19 天前历史提交

文件	最后提交记录	最后更新时间
cLexer.ml	PIDENT with exact ident and PKEYWORD have type `unit p` This means `x = IDENT "bla"` binds x to `()` instead of `"bla"`. Since binding to an exact value is useless no such code appears in the code base. TODO same transformation for FIELD NUMBER etc	21 天前
cLexer.mli	PIDENT with exact ident and PKEYWORD have type `unit p` This means `x = IDENT "bla"` binds x to `()` instead of `"bla"`. Since binding to an exact value is useless no such code appears in the code base. TODO same transformation for FIELD NUMBER etc	21 天前
dune	Remove compat coq-core libraries (not executables) Keep coq-core.kernel because it's used by dune coq mode.	3 个月前
extend.ml	metasyntax convert to token at the same time as we check for keyword needed instead of delaying to egramrocq	7 个月前
extend.mli	metasyntax convert to token at the same time as we check for keyword needed instead of delaying to egramrocq	7 个月前
g_constr.mlg	Make `f (x:=e)%s` parse as `f (x:=e%s)` instead of `(f (x:=e))%s` This also makes it stop relying on level tolerance. Fix #22324	19 天前
g_constr.mli	Use `;` instead of `|` to separate sorts and univs (eg `Type@{s;u}`)	1 年前
g_prim.mlg	Gramlib: more level recovery warnings When asked to parse a level beyond the last existing level, we parse the last existing level instead as a recovery.	11 个月前
g_prim.mli	Rename the Pcoq module into Procq.	1 年前
notation_gram.mli	Inline binder_constr cf #21670 Mostly backwards compatible	5 个月前
notgram_ops.ml	Abstract away the Summary reference type. There is no reason to expose this type as the usual OCaml reference type, and doing so prevents experimenting with more clever implementations where the liboject internals can track the references in a different way.	19 天前
notgram_ops.mli	Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}.	1 年前
pcoq.ml	Introduce a deprecated module alias for Pcoq.	1 年前
pcoq.mli	Introduce a deprecated module alias for Pcoq.	1 年前
procq.ml	Make `f (x:=e)%s` parse as `f (x:=e%s)` instead of `(f (x:=e))%s` This also makes it stop relying on level tolerance. Fix #22324	19 天前
procq.mli	Make `f (x:=e)%s` parse as `f (x:=e%s)` instead of `(f (x:=e))%s` This also makes it stop relying on level tolerance. Fix #22324	19 天前
tok.ml	PIDENT with exact ident and PKEYWORD have type `unit p` This means `x = IDENT "bla"` binds x to `()` instead of `"bla"`. Since binding to an exact value is useless no such code appears in the code base. TODO same transformation for FIELD NUMBER etc	21 天前
tok.mli	PIDENT with exact ident and PKEYWORD have type `unit p` This means `x = IDENT "bla"` binds x to `()` instead of `"bla"`. Since binding to an exact value is useless no such code appears in the code base. TODO same transformation for FIELD NUMBER etc	21 天前