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
*
Minor fix in documentation
Matthieu Sozeau
2016-11-05
*
Do not print dependent evars by default (expensive)
Matthieu Sozeau
2016-11-05
*
More precise refine compatibility
Matthieu Sozeau
2016-11-05
*
Quick fix of tactic parsing while Load-ing in coqide.
Hugo Herbelin
2016-11-04
*
Test for #4966 ("auto" wrongly seen as "auto with *" when in position of ident).
Hugo Herbelin
2016-11-04
*
Fix #3441 Use pf_get_type_of to avoid blowup
Matthieu Sozeau
2016-11-04
*
Fix refine in compatibility mode
Matthieu Sozeau
2016-11-04
*
Fix #4837: ./configure -local makes coqdep issue many warnings
Maxime Dénès
2016-11-04
*
Merge remote-tracking branch 'github/pr/335' into v8.6
Maxime Dénès
2016-11-04
|
\
*
\
Merge remote-tracking branch 'github/pr/336' into v8.6
Maxime Dénès
2016-11-04
|
\
\
*
|
|
Add documentation for [Set Warnings] and the -w option.
Cyprien Mangin
2016-11-04
*
|
|
Silence option deprecation warnings in the compat file
Jason Gross
2016-11-04
*
|
|
Remove an OCaml 4.02 construct.
Maxime Dénès
2016-11-03
*
|
|
Merge remote-tracking branch 'github/pr/340' into v8.6
Maxime Dénès
2016-11-03
|
\
\
\
*
\
\
\
Merge remote-tracking branch 'github/pr/341' into v8.6
Maxime Dénès
2016-11-03
|
\
\
\
\
|
*
|
|
|
Better Arguments compatibility.
Maxime Dénès
2016-11-02
|
/
/
/
/
|
*
|
|
Fix various shortcomings of the warnings infrastructure.
Maxime Dénès
2016-11-02
|
*
|
|
Put string between quotes when printing an option value.
Maxime Dénès
2016-11-02
|
/
/
/
*
|
|
Fix spurious OCaml Warning 56 in TACTIC EXTEND macros.
Pierre-Marie Pédrot
2016-10-30
*
|
|
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-29
|
\
\
\
*
|
|
|
Removing dead code.
Hugo Herbelin
2016-10-29
*
|
|
|
Fixing error localisation bug introduced in fixing #5142 (21e1d501e17c).
Hugo Herbelin
2016-10-29
*
|
|
|
Fixing #5164 (regression in locating error in argument of "refine").
Hugo Herbelin
2016-10-29
*
|
|
|
Merge remote-tracking branch 'github/pr/321' into v8.6
Maxime Dénès
2016-10-28
|
\
\
\
\
*
\
\
\
\
Merge remote-tracking branch 'github/pr/319' into v8.6
Maxime Dénès
2016-10-28
|
\
\
\
\
\
*
\
\
\
\
\
Merge commit 'fccbd64' into v8.6
Maxime Dénès
2016-10-28
|
\
\
\
\
\
\
|
*
|
|
|
|
|
[build] Add a target to install the META file.
Emilio Jesus Gallego Arias
2016-10-28
|
*
|
|
|
|
|
[build] META file to enable plugin linking with ocamlfind.
Emilio Jesus Gallego Arias
2016-10-28
*
|
|
|
|
|
|
Merge remote-tracking branch 'github/pr/337' into v8.6
Maxime Dénès
2016-10-28
|
\
\
\
\
\
\
\
|
|
|
|
|
*
|
|
Fixing #5161 (case of a notation with unability to detect a recursive binder).
Hugo Herbelin
2016-10-27
|
*
|
|
|
|
|
|
Add missing dot to impargs error message.
Maxime Dénès
2016-10-27
|
*
|
|
|
|
|
|
Proper fix for #3753 (anomaly with implicit arguments and renamings)
Maxime Dénès
2016-10-27
|
*
|
|
|
|
|
|
Complete overhaul of the Arguments vernacular.
Maxime Dénès
2016-10-27
*
|
|
|
|
|
|
|
Using msg_info for info_auto and info_eauto (PR #324).
Hugo Herbelin
2016-10-26
*
|
|
|
|
|
|
|
STM: make ~valid state id non optional from APIs
Enrico Tassi
2016-10-26
*
|
|
|
|
|
|
|
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-26
|
\
\
\
\
\
\
\
\
|
|
|
_
|
_
|
_
|
/
/
/
|
|
/
|
|
|
|
|
|
|
*
|
|
|
|
|
|
Merge remote-tracking branch 'github/pr/338' into v8.5
Maxime Dénès
2016-10-25
|
|
\
\
\
\
\
\
\
|
|
*
|
|
|
|
|
|
Remove warning now that info_auto is fixed.
Théo Zimmermann
2016-10-25
|
|
|
|
|
|
|
*
|
Remove v62 from the refman.
Théo Zimmermann
2016-10-25
|
|
|
|
|
|
|
*
|
Remove v62 from the codebase.
Théo Zimmermann
2016-10-25
|
*
|
|
|
|
|
|
|
Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)."
Maxime Dénès
2016-10-25
|
|
/
/
/
/
/
/
/
*
|
|
|
|
|
|
|
Merge commit 'a799600' into v8.6
Maxime Dénès
2016-10-25
|
\
\
\
\
\
\
\
\
|
*
|
|
|
|
|
|
|
That Function is unable to create a Fixpoint equation is a user problem,
Yves Bertot
2016-10-25
|
|
*
|
|
|
|
|
|
Update CHANGES.
Maxime Dénès
2016-10-25
|
|
*
|
|
|
|
|
|
Bump version number to 8.5pl3.
Maxime Dénès
2016-10-25
|
|
*
|
|
|
|
|
|
Merge remote-tracking branch 'github/pr/333' into v8.5
Maxime Dénès
2016-10-25
|
|
|
\
\
\
\
\
\
\
|
|
*
\
\
\
\
\
\
\
Merge remote-tracking branch 'github/pr/329' into v8.5
Maxime Dénès
2016-10-25
|
|
|
\
\
\
\
\
\
\
\
*
|
|
\
\
\
\
\
\
\
\
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-24
|
\
\
\
\
\
\
\
\
\
\
\
|
|
|
/
/
/
/
/
/
/
/
/
|
|
/
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
|
|
Adding a test for #4398 (interpretation scopes for "match goal").
Hugo Herbelin
2016-10-24
*
|
|
|
|
|
|
|
|
|
|
Rename lia.cache into .lia.cache in the test-suite Makefile.
Maxime Dénès
2016-10-24
[next]
Matthieu Sozeau
Hugo Herbelin
Maxime Dénès
Cyprien Mangin
Jason Gross
Pierre-Marie Pédrot
Emilio Jesus Gallego Arias
Enrico Tassi
Théo Zimmermann
Yves Bertot