index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
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
Fix outdated description in RefMan.
Théo Zimmermann
2017-05-02
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#597: Fixing #5487 (v8.5 regression on ltac-matching expressions with...
Maxime Dénès
2017-05-02
Merge PR#582: Fix warnings
Maxime Dénès
2017-05-02
Merge PR#589: remove unneeded -emacs flag in coq-prog-args in test-suite files
Maxime Dénès
2017-05-02
Merge PR#599: Repairing `Set Rewriting Schemes`
Maxime Dénès
2017-05-02
Merge PR#596: Fix for bug 5507. Mispelt de Bruijn.
Maxime Dénès
2017-05-02
Avoiding registering files from _build_ci when not calling Makefile.ci.
Hugo Herbelin
2017-05-02
Merge PR#595: Avoiding registering files from _build_ci for computing depende...
Maxime Dénès
2017-05-01
Add bmsherman/topology to the ci
Jason Gross
2017-05-01
Fixing Set Rewriting Schemes bugs introduced in v8.5.
Hugo Herbelin
2017-05-01
More consistent writing of de Bruijn.
Théo Zimmermann
2017-05-01
remove unneeded -emacs flag to coq-prog-args
Paul Steckler
2017-05-01
Removing dead code in Autorewrite.
Pierre-Marie Pédrot
2017-05-01
Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).
Hugo Herbelin
2017-05-01
Really fixing #2602 which was wrongly working because of #5487 hiding the cause.
Hugo Herbelin
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
Answer to db28e827d: I did test the commit on test-suite but for some
Hugo Herbelin
2017-04-30
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-29
Suppress warning message in stdlib.
Guillaume Melquiond
2017-04-28
Revert "Fixing #5487 (v8.5 regression on ltac-matching expressions with evars)."
Maxime Dénès
2017-04-28
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
Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).
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-27
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
Micromega: do not use Filename.temp_dir_path, remove unused values
Gaetan Gilbert
2017-04-27
Remove unused constructors
Gaetan Gilbert
2017-04-27
Add [_] prefix to unused values which maybe should be kept
Gaetan Gilbert
2017-04-27
Remove some unused values and types
Gaetan Gilbert
2017-04-27
Rename Sos_lib.(||) -> parser_or to avoid (deprecated) Pervasives.or
Gaetan Gilbert
[prev]
[next]