coq

coq copied to clipboard

Make focus command and goal selection for query commands independent of ltac1

1

Fix #18351

SkySkimmer

Ltac2 `assert` scope: intern and typecheck types as types

1

Fix #15094

SkySkimmer

Ltac2: importing a mutable definition does not undo its mutations

5

cf #10556 The previous behaviour can be gotten by doing eg ~~~coq (* auxiliary definition to avoid repeating it, if it's a simple expression it can also be inlined *)...

SkySkimmer

Remove the Lforce node from the generic lambda AST.

6

We move the code responsible from the generation of the forcing of lazy constants in the native compiler to the second compilation phase. This also has the nice side-effect of...

ppedrot

Propagate the unfolded status of primitive projections to parsing and printing

1

This is an experimental PR propagating the unfolded status of primitive projections to parsing and printing so that special parsing/printing notations can be used to refer to them. In the...

herbelin

Adding "Body", synonymous of "Proof", for interactively-defined definitions

8

See discussion at coq/ceps#42. We introduce `Body` as a synonymous of `Proof` to delimit the beginning of a definition by tactics. When used in the form `Body c`, it indicates...

herbelin

[Experiment] Hack a global fixpoint expansion in conversion.

18

Quick and dirty experiment following the Coq call. Rather than implementing a full-blown refolding of fixpoint everywhere, we experiment with refolding when converting only.

ppedrot

Incorrect characterization of computational terms in native_compute

4

```coq (* coqc -native-compiler yes bar.v *) Fixpoint fact n := match n with S n' => n * fact n' | O => 1 end. Definition large : nat...

silene

Extend the Extraction Plugin to synthesise OCaml external and callback definitions for interfacing C/C++

44

This pull request implements the proposal in issue #18212 . The documentation markup files are already updated accordingly. I am very open for remarks and critics and I hope that...

eladrion

CoqIDE UI improvements and fixes

20

Hello. Thank you for providing such good libre software. This week, I’ve worked on improving the UI of CoqIDE, especially the Preferences dialog. Indeed, I’ve started to use CoqIDE at...

Frigory33