index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2016-11-10
Updating a comment in test-suite.
Hugo Herbelin
2016-11-08
Merge commit 'b385fbb' into v8.6
Maxime Dénès
2016-11-08
Use pf_get_type_of to avoid blowup in pose proof of large proof terms
Matthieu Sozeau
2016-11-08
Merge remote-tracking branch 'github/pr/348' into v8.6
Maxime Dénès
2016-11-08
Update documentation of Arguments after recent changes.
Maxime Dénès
2016-11-08
Rewording from Enrico
Matthieu Sozeau
2016-11-07
After Emilio's comment.
Matthieu Sozeau
2016-11-07
Merge remote-tracking branch 'github/pr/339' into v8.6
Maxime Dénès
2016-11-07
Mention notypeclasses refine in CHANGES
Matthieu Sozeau
2016-11-07
CHANGES for this branch.
Matthieu Sozeau
2016-11-07
Document two new variants of refine
Matthieu Sozeau
2016-11-07
Fixes to compile with ocaml 4.01
Matthieu Sozeau
2016-11-07
More accurate contributor list.
Matthieu Sozeau
2016-11-07
Hugo and Maxime's 2nd pass of comments
Matthieu Sozeau
2016-11-07
Merge commit 'e6edb33' into v8.6
Maxime Dénès
2016-11-07
Improve formatting of a message in [Arguments].
Maxime Dénès
2016-11-07
Fix #5181: [Arguments] no longer correctly checks the length of arguments lists
Maxime Dénès
2016-11-07
Fix #5182: "Arguments names must be distinct." is bogus and underinformative
Maxime Dénès
2016-11-07
More explicit name for status of unification constraints.
Maxime Dénès
2016-11-06
Hugo's comments
Matthieu Sozeau
2016-11-06
Maxime's comments
Matthieu Sozeau
2016-11-06
Fixes from Enrico's review
Matthieu Sozeau
2016-11-05
Not using style tags when translating/beautifying a file.
Hugo Herbelin
2016-11-05
Removing a special treatment for empty lines in comments.
Hugo Herbelin
2016-11-05
Removing obsolete parsing of strings à la v7 in comments.
Hugo Herbelin
2016-11-05
Credits for 8.6
Matthieu Sozeau
2016-11-05
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-04
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-03
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
Rework search_strategy option handling
Matthieu Sozeau
2016-11-03
Internal API change to typeclasses eauto.
Théo Zimmermann
2016-11-03
Do not shelve non-class subgoals but fail, it should
Matthieu Sozeau
2016-11-03
Fix test-suite files relying on tcs bugs
Matthieu Sozeau
2016-11-03
Fixed bug #4095.
Matthieu Sozeau
2016-11-03
typeclasses eauto Implem/doc of shelving strategy
Matthieu Sozeau
2016-11-03
Fix [typeclasses eauto with] and nopattern hints
Matthieu Sozeau
2016-11-03
Fix handling of only_classes at toplevel
Matthieu Sozeau
2016-11-03
Test new syntax for hints and typeclass options
Matthieu Sozeau
2016-11-03
Handle Unique Solutions flag.
Matthieu Sozeau
[next]