index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Fixing #4499 (not using unnamed record field in {| |} notation).
Hugo Herbelin
2017-04-07
*
Merge branch 'origin/v8.5' into v8.6.
Hugo Herbelin
2017-04-06
|
\
*
|
Fixing #5454 (an assert false with 'pat).
Hugo Herbelin
2017-04-05
*
|
Merge PR#535: Fix #5435: [Eval native_compute in] raises anomaly.
Maxime Dénès
2017-04-04
|
\
\
|
*
|
Test file for #5435: [Eval native_compute in] raises anomaly.
Maxime Dénès
2017-04-04
|
*
|
Fix bug #5435: [Eval native_compute in] raises anomaly.
Maxime Dénès
2017-04-04
|
/
/
*
|
Merge PR#533: Instances should obey universe binders even when defined by tac...
Maxime Dénès
2017-04-03
|
\
\
|
*
|
Instances should obey universe binders even when defined by tactics.
Gaetan Gilbert
2017-04-03
|
/
/
*
|
Add test file for #4957.
Maxime Dénès
2017-04-03
*
|
Merge PR#463: Run non-tactic comands without resilient_command
Maxime Dénès
2017-03-30
|
\
\
*
\
\
Merge PR#514: [travis] Backport from trunk: VST
Maxime Dénès
2017-03-29
|
\
\
\
|
|
*
|
Run non-tactic comands without resilient_command
Tej Chajed
2017-03-29
|
|
/
/
|
/
|
|
|
*
|
[travis] Backport from trunk: VST
Emilio Jesus Gallego Arias
2017-03-24
|
/
/
*
|
Merge PR#476: [future] Be eager when "chaining" already resolved future values.
Maxime Dénès
2017-03-24
|
\
\
*
\
\
Merge PR#475: Opaque side effects
Maxime Dénès
2017-03-24
|
\
\
\
*
\
\
\
Merge PR#507: Intern names bound in match patterns
Maxime Dénès
2017-03-23
|
\
\
\
\
|
|
*
|
|
Documenting the API of side-effects.
Pierre-Marie Pédrot
2017-03-23
|
|
*
|
|
Using a dedicated datastructure for side effect ordering.
Pierre-Marie Pédrot
2017-03-23
|
|
*
|
|
Making the side_effects type opaque.
Pierre-Marie Pédrot
2017-03-23
|
|
/
/
/
|
/
|
|
|
|
*
|
|
Intern names bound in match patterns
Tej Chajed
2017-03-23
*
|
|
|
Merge PR#497: [travis] [8.6.only] Backport latest changes from trunk.
Maxime Dénès
2017-03-23
|
\
\
\
\
*
\
\
\
\
Merge PR#495: funind: Ignore missing info for current function
Maxime Dénès
2017-03-23
|
\
\
\
\
\
|
|
_
|
/
/
/
|
/
|
|
|
|
*
|
|
|
|
Add empty Extraction.v and FunInd.v to prepare landing of PR#220.
Maxime Dénès
2017-03-23
*
|
|
|
|
Merge PR#491: Do not typecheck twice the type of opaque constants.
Maxime Dénès
2017-03-23
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR#480: show unused intro pattern warning
Maxime Dénès
2017-03-22
|
\
\
\
\
\
\
|
|
|
|
*
|
|
[travis] [8.6.only] Backport latest changes from trunk.
Emilio Jesus Gallego Arias
2017-03-22
|
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
|
|
|
*
|
|
funind: Ignore missing info for current function
Tej Chajed
2017-03-22
|
|
_
|
/
/
/
|
/
|
|
|
|
|
|
*
|
|
Add a few comments in term_typing.ml.
Maxime Dénès
2017-03-21
|
|
*
|
|
Do not typecheck twice the type of opaque constants.
Maxime Dénès
2017-03-21
|
|
/
/
/
|
/
|
|
|
*
|
|
|
Merge PR#430: make `emit' tail recursive
Maxime Dénès
2017-03-20
|
\
\
\
\
|
*
|
|
|
In the Kami project, that causes a stack overflow in one of the example files
Paul Steckler
2017-03-20
|
/
/
/
/
|
|
*
/
[future] Use eager evaluation for chaining values.
Emilio Jesus Gallego Arias
2017-03-20
|
|
/
/
|
/
|
|
*
|
|
Merge PR#429: Don't require printing-only notation to be productive
Maxime Dénès
2017-03-17
|
\
\
\
*
\
\
\
Merge PR#465: Fix #5132: coq_makefile generates incorrect install goal
Maxime Dénès
2017-03-14
|
\
\
\
\
|
*
|
|
|
Fix #5132: coq_makefile generates incorrect install goal
Vadim Zaliva
2017-03-14
|
|
|
*
|
Fix 3 unused-intro-pattern warnings in stdlib.
Théo Zimmermann
2017-03-14
|
|
|
*
|
Show unused-intro-pattern warning.
Théo Zimmermann
2017-03-14
*
|
|
|
|
Merge PR#359: Fix bug 4969, autoapply was not tagging shelved subgoals correc...
Maxime Dénès
2017-03-10
|
\
\
\
\
\
*
|
|
|
|
|
[travis] Move GeoCoq to allow fail.
Emilio Jesus Gallego Arias
2017-03-10
*
|
|
|
|
|
Merge PR#452: [ltac] Move dummy plugin to plugins folder.
Maxime Dénès
2017-03-07
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR#453: [travis] Backport trunk's travis support.
Maxime Dénès
2017-03-07
|
\
\
\
\
\
\
\
|
|
_
|
_
|
/
/
/
/
|
/
|
|
|
|
|
|
|
|
*
|
|
|
|
[ltac] Move dummy plugin to plugins folder.
Emilio Jesus Gallego Arias
2017-03-03
|
|
/
/
/
/
/
|
/
|
|
|
|
|
|
*
|
|
|
|
[travis] Backport trunk's travis support.
Emilio Jesus Gallego Arias
2017-03-02
|
/
/
/
/
/
|
|
|
|
*
Fixing anomaly on unsupported key in interactive ltac debug.
Hugo Herbelin
2017-02-24
|
|
|
|
*
Fixing a little bug in printing ex2 (type was printed "_" by default).
Hugo Herbelin
2017-02-23
|
|
|
|
*
Fixing a little bug in using the "where" clause for inductive types.
Hugo Herbelin
2017-02-23
*
|
|
|
|
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2017-02-22
|
\
\
\
\
\
|
|
|
_
|
_
|
/
|
|
/
|
|
|
*
|
|
|
|
Add empty ltac_plugin file for forward compatibility.
Maxime Dénès
2017-02-21
*
|
|
|
|
Fixing #5339 (anomaly with 'pat in record parameters).
Hugo Herbelin
2017-02-16
|
|
|
*
|
reject notations that are both 'only printing' and 'only parsing'
Ralf Jung
2017-02-16
[next]
Hugo Herbelin
Maxime Dénès
Gaetan Gilbert
Tej Chajed
Emilio Jesus Gallego Arias
Pierre-Marie Pédrot
Paul Steckler
Vadim Zaliva
Théo Zimmermann
Ralf Jung