index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2020-05-15
Update docgram following #12122 and #12229.
Théo Zimmermann
2020-05-15
Merge PR #12323: Fixes #12322: anomaly when printing "fun" binders with impli...
Emilio Jesus Gallego Arias
2020-05-15
Merge PR #11979: Add a rudimentary script to generate release changelog.
Emilio Jesus Gallego Arias
2020-05-15
Clarify release-process.md
Enrico Tassi
2020-05-15
Merge PR #11948: Hexadecimal numerals
Hugo Herbelin
2020-05-15
Merge PR #11755: [exn] [tactics] improve backtraces on monadic errors
Pierre-Marie Pédrot
2020-05-15
Merge PR #12243: Add a note on build-time dependencies to INSTALL.md.
Emilio Jesus Gallego Arias
2020-05-15
Fix typo.
Théo Zimmermann
2020-05-15
Merge PR #11992: do not re-export ListNotations from Program
Anton Trunov
2020-05-15
Merge PR #12032: [win] Elpi, Coq-Elpi and HB
Michael Soegtrop
2020-05-15
[interp] Register printers for InternalizationError instead of ad-hoc hanlding.
Emilio Jesus Gallego Arias
2020-05-15
[misc] Better preserve backtraces in several modules
Emilio Jesus Gallego Arias
2020-05-14
Merge PR #12256: Move the static check of evaluability in unfold tactic to ru...
Hugo Herbelin
2020-05-14
[exn] [tactics] improve backtraces on monadic errors
Emilio Jesus Gallego Arias
2020-05-14
Add advisories on OCaml setup to INSTALL.md.
Théo Zimmermann
2020-05-14
Merge PR #12296: Fixes #12234: wrong environment for Show Proof
Gaëtan Gilbert
2020-05-14
Merge PR #12327: Add a changelog for 8.11.2.
Théo Zimmermann
2020-05-14
Merge PR #11922: No more local reduction functions in Reductionops.
Maxime Dénès
2020-05-14
Add a changelog for 8.11.2.
Pierre-Marie Pédrot
2020-05-14
Merge PR #12312: Clarify the documentation for merging PRs with overlays
Théo Zimmermann
2020-05-14
Fix title level and a build failure.
Théo Zimmermann
2020-05-14
Fix conflicts with latest master.
Théo Zimmermann
2020-05-14
Add some markers of origin.
Théo Zimmermann
2020-05-14
Reintroduce leftover parts; update index files; small fixes.
Théo Zimmermann
2020-05-14
Adding changelog.
Pierre-Marie Pédrot
2020-05-14
Remove an outdated piece of documentation about limitations of unfold.
Pierre-Marie Pédrot
2020-05-14
Tweak the error message of reference internalization.
Pierre-Marie Pédrot
2020-05-14
Add test for #11727, which was indirectly fixed by this PR.
Pierre-Marie Pédrot
2020-05-14
Generalize the interpretation of syntactic notation as reference to their head.
Pierre-Marie Pédrot
2020-05-14
Move the static check of evaluability in unfold tactic to runtime.
Pierre-Marie Pédrot
2020-05-14
Added change log.
Hugo Herbelin
2020-05-14
Fixes #12234 (wrong environment for Show Proof).
Hugo Herbelin
2020-05-14
Refactoring of the first part of the reference manual.
Théo Zimmermann
2020-05-14
Preserve Implicit arguments file.
Théo Zimmermann
2020-05-14
Remove Canonical structures from Implicit arguments.
Théo Zimmermann
2020-05-14
Merge doc on Canonical structures from two origins.
Théo Zimmermann
2020-05-14
Merge PR #12313: Make explicit that UGraph lower bounds are only of two kinds.
Gaëtan Gilbert
2020-05-14
Move Canonical structures file into new location.
Théo Zimmermann
2020-05-14
Merge PR #12320: [ci] [sf] Fix SF build.
Gaëtan Gilbert
2020-05-14
Add Canonical structure declarations to Canonical structures file.
Théo Zimmermann
2020-05-14
Extract Canonical structures from Implicit arguments.
Théo Zimmermann
2020-05-14
Split Gallina extensions into multiple files.
Théo Zimmermann
2020-05-14
Split Gallina into multiple files.
Théo Zimmermann
2020-05-14
Split parts of CIC into multiple files.
Théo Zimmermann
2020-05-14
Create new file on Functions and Assumptions.
Théo Zimmermann
2020-05-14
Extract functions and assumptions.
Théo Zimmermann
2020-05-14
Merge definitions and type casts in same file.
Théo Zimmermann
2020-05-14
Create new file on Definitions.
Théo Zimmermann
2020-05-14
Extract Definitions from Gallina.
Théo Zimmermann
2020-05-14
Add type casts to new Definitions file.
Théo Zimmermann
[prev]
[next]