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-04-27
Minor doc improvement.
Théo Zimmermann
2019-04-27
[refman] Fix typo.
Théo Zimmermann
2019-04-27
[ci/gitlab] Remove after_switch message (not useful anymore).
Théo Zimmermann
2019-04-27
Amending CYGWIN fix in 63e7fb56923 so that it does not add a warning on MacOS.
Hugo Herbelin
2019-04-26
Merge PR #9998: coq_makefile: do not pass -opt/-byte to coqc (fix #9974)
Emilio Jesus Gallego Arias
2019-04-26
Merge PR #9981: [dune] Build coqc.byte executable.
Théo Zimmermann
2019-04-26
Merge PR #9990: [opam] Use version to provide better package bounds.
Théo Zimmermann
2019-04-26
Merge PR #10001: Add a typing colon in the output of the Search ssreflect ver...
Enrico Tassi
2019-04-26
[opam] Use version to provide better package bounds.
Emilio Jesus Gallego Arias
2019-04-25
[vernac] [ast] Make location info an attribute of vernaculars.
Emilio Jesus Gallego Arias
2019-04-25
Merge PR #9999: Fix PKG in ide/.merlin.in for gtk3
Emilio Jesus Gallego Arias
2019-04-25
CoqIDE: install icons on macOS
Vincent Laporte
2019-04-25
inferCumulativity: shortcut for all-Invariant inductives
Gaëtan Gilbert
2019-04-25
Add a typing colon in the output of the Search ssreflect vernacular
Erik Martin-Dorel
2019-04-25
Fix PKG in ide/.merlin.in for gtk3
Gaëtan Gilbert
2019-04-25
CoqIDE: fix open-file dialog on macOS
Vincent Laporte
2019-04-25
coq_makefile: do not pass -opt/-byte to coqc (fix #9974)
Enrico Tassi
2019-04-25
Merge Ltac2 plugin
Maxime Dénès
2019-04-25
Prepare merge into Coq
Maxime Dénès
2019-04-24
Merge PR #9988: [refman] Properly define token regexp.
Clément Pit-Claudel
2019-04-24
Merge PR #9989: [refman] Fix a quoting problem.
Clément Pit-Claudel
2019-04-24
[refman] Fix a quoting problem.
Théo Zimmermann
2019-04-24
[refman] Properly define token regexp.
Théo Zimmermann
2019-04-24
[coq_makefile] Enforce warn_error for plugins.
Emilio Jesus Gallego Arias
2019-04-24
Fix proof bullet error helper (nosuchgoal)
Gaëtan Gilbert
2019-04-24
[proof] Fix proof bullet error helper which was implemented as a hook
Emilio Jesus Gallego Arias
2019-04-24
Allocate only one evar when applying a group of conversion tactics.
Pierre-Marie Pédrot
2019-04-24
Code factorization in conversion tactics.
Pierre-Marie Pédrot
2019-04-24
[dune] Build coqc.byte executable.
Emilio Jesus Gallego Arias
2019-04-23
Deprecate the *_no_check variants of conversion tactics.
Pierre-Marie Pédrot
2019-04-23
Merge PR #9962: [native compiler] Encoding of constructors based on tags
Pierre-Marie Pédrot
2019-04-23
[ssr] set under's tactic argument at LEVEL 3
Erik Martin-Dorel
2019-04-23
[ssr] under: optimization of the tactic for (under eq_bigl => *)
Erik Martin-Dorel
2019-04-23
[ssr] Define over as a rewrite rule & Merge 'Under[ _ ] notations
Erik Martin-Dorel
2019-04-23
[doc] ssr_under: a few improvements
Enrico Tassi
2019-04-23
[ssr] under: Fix the defective form ("=> [*|*]" implied) and its doc
Erik Martin-Dorel
2019-04-23
[ssr] Add small output test for "under eq_G => m do rewrite subnn"
Erik Martin-Dorel
2019-04-23
[ssr] under: Fix and extend the documentation
Erik Martin-Dorel
2019-04-23
[ssr] under: Add iff support in side-conditions
Erik Martin-Dorel
2019-04-23
Merge PR #9889: Fix pretty-printing of primitive integers
Maxime Dénès
2019-04-23
Merge PR #9978: Remove duplicate copy of _warn_if_duplicate_name.
Gaëtan Gilbert
2019-04-23
Merge PR #9973: update elpi to version 1.2
Gaëtan Gilbert
2019-04-23
[ssr] under: use varnames from the 1st ipat with multi-goal under lemmas
Erik Martin-Dorel
2019-04-23
[ssr] new syntax for the under tactic
Enrico Tassi
2019-04-23
[ssr] under: Simplify the over tactic
Erik Martin-Dorel
2019-04-23
[ssr] under: Add doc for {under, over} & Add entry in CHANGES.md
Erik Martin-Dorel
2019-04-23
[ssr] under: Add comment to justify the need for check_numgoals
Erik Martin-Dorel
2019-04-23
[ssr] over: Expose the new type of tactic for Ssrfwd.overtac
Erik Martin-Dorel
2019-04-23
[ssr] Remove the unify_helper tactic that appears unnecessary
Erik Martin-Dorel
2019-04-23
[ssr] under: Fix rewrite goals order when called from under
Erik Martin-Dorel
[prev]
[next]