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-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
2019-02-28
Constructor type information uses the expanded form.
Pierre-Marie Pédrot
2019-02-28
Overlays for coq/coq#9389 implicits API cleanup
Gaëtan Gilbert
2019-02-23
[vernac] Unify declaration hooks.
Emilio Jesus Gallego Arias
2019-02-22
overlay for Equations
Enrico Tassi
2019-02-17
Separate variance and universe fields in inductives.
Gaëtan Gilbert
2019-02-12
[tactics] Remove dependency of abstract on global proof state.
Emilio Jesus Gallego Arias
2019-02-08
Update overlay file
Matthieu Sozeau
2019-02-08
Add overlay for Equations
Matthieu Sozeau
2019-02-08
Add overlays for unicoq and mtac2
Matthieu Sozeau
2019-02-05
Overlays
Maxime Dénès
2019-02-04
Overlays.
Maxime Dénès
2019-01-24
Add Overlays
Maxime Dénès
[next]