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
*
Upgrading some local function as a general-purpose combinator Option.List.map.
Hugo Herbelin
2017-05-05
*
Adding a test-suite pattern-unification example that Econstr fixed.
Hugo Herbelin
2017-05-05
*
Merge PR#610: Improve documentation of assert / pose proof / specialize.
Maxime Dénès
2017-05-05
|
\
*
\
Merge PR#605: Report a useful error for dependent induction
Maxime Dénès
2017-05-05
|
\
\
*
\
\
Merge PR#454: Printing unfocussed goals and toward a pg plugin.
Maxime Dénès
2017-05-05
|
\
\
\
*
\
\
\
Merge PR#593: Functional choice <-> [inhabited] and [forall] commute
Maxime Dénès
2017-05-05
|
\
\
\
\
*
|
|
|
|
Remove unused open.
Maxime Dénès
2017-05-05
*
|
|
|
|
Merge PR#544: Anonymous universes
Maxime Dénès
2017-05-05
|
\
\
\
\
\
|
|
|
|
|
*
Improve documentation of assert / pose proof / specialize.
Théo Zimmermann
2017-05-04
|
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
*
|
Warning removed.
Pierre Courtieu
2017-05-04
|
|
|
*
|
labelizing arguments
Pierre Courtieu
2017-05-04
|
|
|
*
|
Adding an option "Printing Unfocused".
Pierre Courtieu
2017-05-04
|
|
_
|
/
/
|
/
|
|
|
*
|
|
|
Merge PR#541: Fixing "decide equality" bug #5449
Maxime Dénès
2017-05-03
|
\
\
\
\
*
\
\
\
\
Merge PR#588: Allow interactive editing of {C,}Morphisms in PG
Maxime Dénès
2017-05-03
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR#386: Better editing of the standard library in coqtop/PG
Maxime Dénès
2017-05-03
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR#602: Fix more warnings
Maxime Dénès
2017-05-03
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR#404: patch for printing types of let bindings
Maxime Dénès
2017-05-03
|
\
\
\
\
\
\
\
\
|
|
|
|
|
|
|
|
*
Report a useful error for dependent induction
Tej Chajed
2017-05-03
|
|
_
|
_
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
Reorganize comment documentation of ChoiceFacts.v
Gaetan Gilbert
2017-05-03
|
|
|
|
|
|
*
|
Type@{_} should not produce a flexible algebraic universe.
Gaetan Gilbert
2017-05-03
|
|
|
|
|
|
*
|
Allow flexible anonymous universes in instances and sorts.
Gaetan Gilbert
2017-05-03
*
|
|
|
|
|
|
|
Merge PR#411: Mention template polymorphism in the documentation.
Maxime Dénès
2017-05-03
|
\
\
\
\
\
\
\
\
|
|
_
|
_
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
applied the patch for printing types of let bindings by @herbelin
Abhishek Anand (@brixpro-home)
2017-05-02
|
|
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
*
|
|
|
|
Remove dead code in native compiler.
Maxime Dénès
2017-05-02
|
|
*
|
|
|
|
Fix two new unused opens.
Maxime Dénès
2017-05-02
|
|
*
|
|
|
|
Remove unused module definition after merging PR#592.
Maxime Dénès
2017-05-02
|
|
/
/
/
/
/
|
/
|
|
|
|
|
*
|
|
|
|
|
Merge PR#592: Fix bug #5501: Universe polymorphism breaks proof involving auto.
Maxime Dénès
2017-05-02
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR#582: Fix warnings
Maxime Dénès
2017-05-02
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR#596: Fix for bug 5507. Mispelt de Bruijn.
Maxime Dénès
2017-05-02
|
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
Merge PR#595: Avoiding registering files from _build_ci for computing depende...
Maxime Dénès
2017-05-02
|
\
\
\
\
\
\
\
\
\
|
|
*
|
|
|
|
|
|
|
More consistent writing of de Bruijn.
Théo Zimmermann
2017-05-01
|
|
*
|
|
|
|
|
|
|
Fix for bug 5507. Mispelt de Bruijn.
Théo Zimmermann
2017-05-01
|
|
/
/
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
Avoiding registering files from _build_ci when not calling Makefile.ci.
Hugo Herbelin
2017-05-01
|
/
/
/
/
/
/
/
/
|
|
|
|
|
|
|
*
Functional choice <-> [inhabited] and [forall] commute
Gaetan Gilbert
2017-04-30
|
|
_
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
*
|
|
|
|
Fix bug #5501: Universe polymorphism breaks proof involving auto.
Pierre-Marie Pédrot
2017-04-30
|
|
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
*
Fixing "decide equality"'s bug #5449.
Hugo Herbelin
2017-04-30
|
|
_
|
_
|
_
|
/
|
/
|
|
|
|
*
|
|
|
|
Suppress warning message in stdlib.
Guillaume Melquiond
2017-04-29
*
|
|
|
|
Revert "Renaming allow_patvar flag of intern_gen into pattern_mode."
Maxime Dénès
2017-04-28
*
|
|
|
|
Revert "Using a more explicit algebraic type for evars of kind "MatchingVar"."
Maxime Dénès
2017-04-28
|
|
|
|
*
Allow interactive editing of {C,}Morphisms in PG
Jason Gross
2017-04-28
|
|
_
|
_
|
/
|
/
|
|
|
|
|
|
*
Add .dir-locals.el and _CoqProject files for emacs stdlib editing
Jason Gross
2017-04-28
|
|
_
|
/
|
/
|
|
*
|
|
Using a more explicit algebraic type for evars of kind "MatchingVar".
Hugo Herbelin
2017-04-28
*
|
|
Renaming allow_patvar flag of intern_gen into pattern_mode.
Hugo Herbelin
2017-04-28
*
|
|
Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...
Maxime Dénès
2017-04-28
|
\
\
\
|
|
*
|
Post-rebase warnings (unused opens and 2 unused values)
Gaetan Gilbert
2017-04-27
|
|
*
|
Enable more warnings, and add -warn-error configure flag
Gaetan Gilbert
2017-04-27
|
|
*
|
Fix 4.04 warnings
Gaetan Gilbert
2017-04-27
|
|
*
|
Remove uses of [Flags.make_silent]
Gaetan Gilbert
2017-04-27
|
|
*
|
Warning 29: non escaped end of line may be non portable
Gaetan Gilbert
2017-04-27
|
|
*
|
Remove unused [open] statements
Gaetan Gilbert
2017-04-27
[next]
Hugo Herbelin
Maxime Dénès
Théo Zimmermann
Pierre Courtieu
Tej Chajed
Gaetan Gilbert
Abhishek Anand (@brixpro-home)
Pierre-Marie Pédrot
Guillaume Melquiond
Jason Gross