index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2019-02-11
Introduce a GADT of well-typed grammar entries in Grammar.
Pierre-Marie Pédrot
2019-02-11
Centralizing the calls to the global mutable grammar in Grammar.
Pierre-Marie Pédrot
2019-02-11
Specialize the intermediate types of the Grammar functor.
Pierre-Marie Pédrot
2019-02-11
Make Grammar truly functorial.
Pierre-Marie Pédrot
2019-02-11
Move most of Gramext into Grammar.
Pierre-Marie Pédrot
2019-02-11
Merge PR #9465: [Nix-CI] Add iris and lambda-rust
Maxime Dénès
2019-02-11
Fix #9508: Unexpected interaction between implicit arguments and primitive pr...
Pierre-Marie Pédrot
2019-02-11
[coqargs] Minor refactoring of error functions.
Emilio Jesus Gallego Arias
2019-02-11
Merge PR #9541: [stm] -async-proofs-tac-j accepts only >= 1 (fix #9533)
Emilio Jesus Gallego Arias
2019-02-11
Merge PR #9543: [ocamldebug] Fix load order after gramlib refactoring.
Gaëtan Gilbert
2019-02-11
Fix #9527: unknown evar in nonterminating [fix] error.
Gaëtan Gilbert
2019-02-11
Merge PR #9522: Update link to refman for master branch.
Vincent Laporte
2019-02-11
[stm] -async-proofs-tac-j accepts only >= 1 (fix #9533)
Enrico Tassi
2019-02-11
[ssr] keep user annotation on views (fix #9538)
Enrico Tassi
2019-02-11
[coqdoc] Add the From keyword
Pierre Roux
2019-02-11
Use math mode more.
Tanaka Akira
2019-02-11
Use {LEFT,RIGHT} DOUBLE QUOTATION MARK.
Tanaka Akira
2019-02-11
Remove a space before closing double-quote.
Tanaka Akira
2019-02-11
[ocamldebug] Fix load order after gramlib refactoring.
Emilio Jesus Gallego Arias
2019-02-11
Merge PR #9478: Remove the comment fields of locations.
Emilio Jesus Gallego Arias
2019-02-11
Merge PR #9534: Workaround for CI not having enough RAM for bedrock2: `-async...
Emilio Jesus Gallego Arias
2019-02-10
Merge PR #9535: [readme] Add link to information about release plans.
Théo Zimmermann
2019-02-10
Change "I" to "I_p".
Tanaka Akira
2019-02-10
Distinguish inductive {definition,inductive}.
Tanaka Akira
2019-02-10
Merge PR #9536: [ci] Remove unused bintray file.
Maxime Dénès
2019-02-09
remove `allow_failure: true` for bedrock2
Samuel Gruetter
2019-02-09
remove VERBOSE=1, gitlab log shows that `-async-proofs-tac-j 1` was indeed pa...
Samuel Gruetter
2019-02-09
Update link to refman and stdlib doc for master branch.
Théo Zimmermann
2019-02-09
[ci] Remove unused bintray file.
Emilio Jesus Gallego Arias
2019-02-09
[coq] Adapt to coq/coq#9137
Emilio Jesus Gallego Arias
2019-02-09
[readme] Add link to information about release plans.
Emilio Jesus Gallego Arias
2019-02-09
Merge pull request coq/ltac2#102 from maximedenes/rm-unknown
Pierre-Marie Pédrot
2019-02-08
Workaround for CI not having enough RAM for bedrock2: `-async-proofs-tac-j 1`
Samuel Gruetter
2019-02-08
Remove VtUnknown classification
Maxime Dénès
2019-02-08
Merge PR #9525: Remove global output_native_objects flag.
Emilio Jesus Gallego Arias
2019-02-08
Merge PR #9523: Make boot flag into a normal option (no global flag).
Emilio Jesus Gallego Arias
2019-02-08
[test-suite] Improve test for async workers.
Emilio Jesus Gallego Arias
2019-02-08
Merge PR #9481: [parsing] Use AST node for main parsing entry.
Enrico Tassi
2019-02-08
Merge PR #9492: [stm] Filter some more arguments that shouldn't be sent to wo...
Enrico Tassi
2019-02-08
Change Primitive message: "is registered" -> "is declared".
Gaëtan Gilbert
2019-02-08
Update overlay file
Matthieu Sozeau
2019-02-08
Merge PR #9504: Add print_pure_econstr signature
Gaëtan Gilbert
2019-02-08
coqargs: use algebraic datatype for -native-compiler
Gaëtan Gilbert
2019-02-08
Remove global output_native_objects flag.
Gaëtan Gilbert
2019-02-08
Make boot flag into a normal option (no global flag).
Gaëtan Gilbert
2019-02-08
Merge pull request coq/ltac2#101 from maximedenes/program-mode-flag
Pierre-Marie Pédrot
2019-02-08
Merge PR #9513: Edit release-process.md to ease upcoming releases of Coq in D...
Théo Zimmermann
2019-02-08
evarsolve transp_state and comments fixes
Matthieu Sozeau
2019-02-08
evarconf transp state and comments fixes
Matthieu Sozeau
2019-02-08
Coercion intf fix
Matthieu Sozeau
[prev]
[next]