index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
dev
/
ci
/
user-overlays
Age
Commit message (
Expand
)
Author
2019-06-13
Merge PR #10319: [STM] Only VtSideeff can be VtNow/VtLater
Enrico Tassi
2019-06-12
Merge PR #10358: [docker] update elpi to 1.3.1
Gaëtan Gilbert
2019-06-11
overlay
Enrico Tassi
2019-06-11
Adding an overlay for Equations.
Pierre-Marie Pédrot
2019-06-11
Overlays for 10319
Gaëtan Gilbert
2019-06-09
[ci] Overlays for move_termination_routine_out
Emilio Jesus Gallego Arias
2019-06-08
Overlays for Elpi + Equations + Mtac2 + fiat parsers + paramcoq.
Hugo Herbelin
2019-06-06
Remove old overlays
Gaëtan Gilbert
2019-06-06
Merge PR #8988: Towards unifying parsing/printing for universe instances and ...
Gaëtan Gilbert
2019-06-04
update overlays
Enrico Tassi
2019-06-04
Overlays for coq/coq#10050 (proof_global API changes)
Gaëtan Gilbert
2019-06-01
Adding overlay for elpi
Hugo Herbelin
2019-05-27
Overlay for mind_kelim change (#10133)
Gaëtan Gilbert
2019-05-24
Adding overlays.
Pierre-Marie Pédrot
2019-05-23
Merge PR #9895: [loadpath] Make loadpath handling self-contained and move to ...
Maxime Dénès
2019-05-23
Merge PR #10185: Remove undocumented Instance : ! syntax
Vincent Laporte
2019-05-22
Merge PR #10177: Fix #10176: shadowing vs automatic class based generalizatio...
Hugo Herbelin
2019-05-21
[loadpath] Further cleanup after merge with MlTop.
Emilio Jesus Gallego Arias
2019-05-21
Overlay for definition-not-visible overhaul
Gaëtan Gilbert
2019-05-21
Overlay for removing Instance: !type syntax
Gaëtan Gilbert
2019-05-17
Overlay for removing Generalized 1st arg
Gaëtan Gilbert
2019-05-14
Merge PR #8893: Moving evars_of_term from constr to econstr
Pierre-Marie Pédrot
2019-05-14
Merge PR #10125: Allow run_tactic to return a value, remove hack from ltac2
Pierre-Marie Pédrot
2019-05-14
Merge PR #10135: Make detyping robust w.r.t. indexed anonymous variables
Pierre-Marie Pédrot
2019-05-14
Overlay for value-returning run_tactic
Gaëtan Gilbert
2019-05-13
Adding overlay for Equations.
Hugo Herbelin
2019-05-13
Merge PR #10076: [Canonical structures] Annotation to field declarations to p...
Enrico Tassi
2019-05-13
Add overlay for Unicoq
Maxime Dénès
2019-05-10
Add overlay for elpi
Vincent Laporte
2019-05-10
Add overlays for coq/coq#10052.
Pierre-Marie Pédrot
2019-05-07
Add overlays.
Pierre-Marie Pédrot
2019-04-20
overlay for elpi
Enrico Tassi
2019-04-16
[ci] Overlays for coq/coq#9165
Emilio Jesus Gallego Arias
2019-04-10
Overlays for Global removal in pretyper
Maxime Dénès
2019-04-05
Merge PR #8764: Add parsing of decimal constants (e.g., 1.02e+01)
Emilio Jesus Gallego Arias
2019-04-02
Merge PR #8984: Declare initial hint databases in prelude
Pierre-Marie Pédrot
2019-04-02
Add overlays
Pierre Roux
2019-04-01
Merge PR #9870: Minor refactoring in canonical structures
Enrico Tassi
2019-03-31
Add overlay
Pierre Roux
2019-03-31
Merge PR #9733: [lexer] keyword protected quotation token for arbitrary text
Pierre-Marie Pédrot
2019-03-31
overlay for ltac2
Enrico Tassi
2019-03-30
Error when [foo.(bar)] is used with nonprojection [bar]
Gaëtan Gilbert
2019-03-30
Overlay for Elpi
Vincent Laporte
2019-03-27
[proof_global] [ci] Overlays for removal of imperative state.
Emilio Jesus Gallego Arias
2019-03-26
Overlays for HoTT, Ltac2, and UniMath
Vincent Laporte
2019-03-22
Merge PR #9602: [kernel] termination checking: backtrack on stuck case, fix, ...
Maxime Dénès
2019-03-20
Add overlays for printer API changes
Maxime Dénès
2019-03-14
Overlays for SProp
Gaëtan Gilbert
2019-03-12
Merge PR #9389: Implement a method for manual declaration of implicits.
Emilio Jesus Gallego Arias
2019-03-12
Merge PR #7819: Ho matching occ sel
Enrico Tassi
[prev]
[next]