index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
toplevel
Age
Commit message (
Expand
)
Author
2016-10-16
Fix bug #5141: Bogus message "Error: Cannot infer type of pattern-matching".
Pierre-Marie Pédrot
2016-10-12
Merge PR #224 into v8.6
Pierre-Marie Pédrot
2016-10-10
Fixing #5133 (error reporting delayed).
Hugo Herbelin
2016-10-09
Moving Pp.comments to CLexer so that Pp is purer (no more side-effect
Hugo Herbelin
2016-10-09
Attaching all extra imperative components of the lexer/parser state to
Hugo Herbelin
2016-10-09
Fixing beautification to file.
Hugo Herbelin
2016-10-07
Fix bug #5125: Bad error message when attempting to use where with Class.
Pierre-Marie Pédrot
2016-10-06
Remove the -no-compat-notations flag.
Maxime Dénès
2016-10-06
Remove the Set Verbose Compat option and turn the warning on by default.
Maxime Dénès
2016-10-05
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-10-05
Fix a bug of Mltop.declare_cache_object.
Pierre-Marie Pédrot
2016-10-04
Quick fix to #4595 (making notations containing "ltac:" unused for printing).
Hugo Herbelin
2016-10-04
Merge remote-tracking branch 'github/pr/305' into v8.6
Maxime Dénès
2016-10-03
Fixing #4970 (confusion between special "{" and non special "{{" in notations).
Hugo Herbelin
2016-10-02
Fix bug #5069: Scheme Equality gives anomalies in sections.
Pierre-Marie Pédrot
2016-10-01
Speed up the Search commands.
Guillaume Melquiond
2016-10-01
Add command 'Set foo Append "bar"' for appending to an option (bug #5109).
Guillaume Melquiond
2016-09-30
Merge remote-tracking branch 'github/pr/299' into v8.6
Maxime Dénès
2016-09-30
Merge remote-tracking branch 'github/pr/281' into v8.6
Maxime Dénès
2016-09-30
In <= 8.5 compat accept "Arguments f /" even if f has arguments (#5112)
Enrico Tassi
2016-09-30
Give name to warning added in (fdfcdc): arguments-ignore-rename-nonimpl
Enrico Tassi
2016-09-30
[pp] Remove duplicate color logger.
Emilio Jesus Gallego Arias
2016-09-29
Fix bug #4798: compat notations should not modify the parser.
Pierre-Marie Pédrot
2016-09-29
Arguments: cleanup + detect discrepancy rename/implicit (#3753)
Enrico Tassi
2016-09-29
Merge branch 'bug4723' into v8.6
Matthieu Sozeau
2016-09-29
Fix bug #4869, allow Prop, Set, and level names in constraints.
Matthieu Sozeau
2016-09-29
fix bug 3683 : adds references to the web site for the bug tracker
Yves Bertot
2016-09-29
Fix bug #5011: Anomaly on [Existing Class].
Pierre-Marie Pédrot
2016-09-29
Cleanup API, making inference_hook optional
Matthieu Sozeau
2016-09-29
Argument : assert does fail if no arg is given (fix #4864)
Enrico Tassi
2016-09-29
-profile-ltac-cutoff alike Show Ltac Profile Cutoff (#5100)
Enrico Tassi
2016-09-28
Fix bug #4723 and FIXME in API for solve_by_tac
Matthieu Sozeau
2016-09-25
The coqtop options -Q and -R do not affect the ML loadpath anymore.
Pierre-Marie Pédrot
2016-09-22
coqc -o now places .glob file near .vo file
Enrico Tassi
2016-09-19
Fix warning when using Variables at toplevel.
Maxime Dénès
2016-09-17
Fix indentation of -profile-ltac in -help
Jason Gross
2016-09-13
coqc: print debug feedback coming from workers
Enrico Tassi
2016-09-10
Avoid putting a useless "toploop" directory in the ML search path if it does ...
Guillaume Melquiond
2016-09-09
Make it explicit when paths are added to the ML search paths.
Guillaume Melquiond
2016-09-08
Avoid canonizing the same paths over and over.
Guillaume Melquiond
2016-08-30
Fix #4941 - ~/.coqrc file confusing locations
Maxime Dénès
2016-08-27
Support qualified identifiers in Show Match (bug #5050).
Guillaume Melquiond
2016-08-25
Do not export an internal function in Namegen.
Pierre-Marie Pédrot
2016-08-24
Properly compute types for assumed section variables (bug #5035).
Guillaume Melquiond
2016-08-24
Merge PR #260: "Fix bug 4842 (Time prints in multiple lines)" into v8.6
Pierre-Marie Pédrot
2016-08-24
Merge PR #258: "Fix newline issues" into v8.6
Pierre-Marie Pédrot
2016-08-23
Arguments: give / after last ! error detection fixed
Enrico Tassi
2016-08-23
fix get_host_port error message (#4724)
Enrico Tassi
2016-08-21
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-08-20
Fixing an anomaly in printing a unification error message.
Hugo Herbelin
[next]