| Age | Commit message (Collapse) | Author |
|---|
|
|
|
notation declarations
Reviewed-by: JasonGross
Reviewed-by: Zimmi48
Ack-by: jfehrle
|
|
|
|
|
|
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
|
|
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
Ack-by: Zimmi48
Ack-by: gares
Reviewed-by: ppedrot
|
|
We deprecate unspecified locality as was done for Hint.
Close #13724
|
|
into `pat:`
Ack-by: Zimmi48
Reviewed-by: jfehrle
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: Zimmi48
Ack-by: JasonGross
|
|
|
|
|
|
|
|
|
|
As discussed in the Coq meeting.
|
|
Co-authored-by: <Théo Zimmermann <theo.zimmermann@inria.fr>
|
|
The syntax is the one of boolean attributes, that is to say
`#[typing($flag={yes,no}]` where `$flag` is one of `guarded`,
`universes`, `positive`.
We had to instrument the pretyper in a few places, it is interesting
that it is doing so many checks.
|
|
|
|
sense
Reviewed-by: Zimmi48
|
|
|
|
|
|
|
|
Reviewed-by: ejgallego
Reviewed-by: Zimmi48
Ack-by: ppedrot
Ack-by: jfehrle
|
|
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
|
|
Reviewed-by: gares
Ack-by: Zimmi48
|
|
|
|
|
|
OCaml and Gallina.
Reviewed-by: jfehrle
Reviewed-by: cpitclaudel
|
|
The smallcaps rendering was inexistent in the PDF version and did not
look good in the HTML version.
|
|
|
|
Actual documentation was interpreted as a comment.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
