index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
Commit message (
Expand
)
Author
Age
*
A hack to fix another regression with Ltac trace report in 8.5. E.g.
Hugo Herbelin
2016-06-18
*
Merge branch 'bug4725' into v8.5
Matthieu Sozeau
2016-06-14
|
\
*
|
Tentatively fixing misguiding error message with "binder" type in
Hugo Herbelin
2016-06-13
*
|
Reserve exception "ConversionFailed" in unification for failure of
Hugo Herbelin
2016-06-12
*
|
Fixing bug in printing CannotSolveConstraint (collision of context names).
Hugo Herbelin
2016-06-12
*
|
Fixing problems introduced in 8.5 with Ltac trace report. E.g.
Hugo Herbelin
2016-06-06
*
|
Revert "Rename Lexer -> CLexer."
Pierre-Marie Pédrot
2016-05-31
|
*
Univs/Program/Function: Fix bug #4725
Matthieu Sozeau
2016-05-26
|
*
Program: remove debug tracing
Matthieu Sozeau
2016-05-26
|
/
*
Fix bug #3887: Better error message for "More than one program with unsolved ...
Pierre-Marie Pédrot
2016-05-09
*
Rename Lexer -> CLexer.
Pierre-Marie Pédrot
2016-05-09
*
Fix bug #4705: coqtop accepts both -emacs and -ideslave.
Pierre-Marie Pédrot
2016-05-03
*
Call hooks when terminating a definition proof (bug #4663).
Guillaume Melquiond
2016-05-03
*
Properly handle notations containing spaces (bug #4538).
Guillaume Melquiond
2016-05-02
*
Building lazily a few debugging messages involving expressions of commands
Hugo Herbelin
2016-04-17
*
Allow to unset the refinement mode of Instance in ML
Matthieu Sozeau
2016-04-07
*
Fix handling of arity of definitional classes.
Matthieu Sozeau
2016-03-24
*
Fix bug #4627: records with no declared arity can be template polymorphic.
Matthieu Sozeau
2016-03-17
*
Fix bug when a sort is ascribed to a Record
Matthieu Sozeau
2016-03-15
*
Adding backtraces to scheme error messages.
Pierre-Marie Pédrot
2016-03-07
*
Rename Ephemeron -> CEphemeron.
Maxime Dénès
2016-03-04
*
Fixing bug #4580: [Set Refine Instance Mode] also used for Program Instance.
Pierre-Marie Pédrot
2016-02-19
*
Improving error message with missing patterns in the presence of
Hugo Herbelin
2016-02-08
*
Fixing bug #3826: "Incompatible module types" is uninformative.
Pierre-Marie Pédrot
2016-01-24
*
Fixing bug #4495: Failed assertion in metasyntax.ml.
Pierre-Marie Pédrot
2016-01-24
*
Implement support for universe binder lists in Instance and Program Fixpoint/...
Matthieu Sozeau
2016-01-23
*
Restore warnings produced by the interpretation of the command line
Hugo Herbelin
2016-01-22
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.
Maxime Dénès
2016-01-15
*
Inclusion of functors with restricted signature is now forbidden (fix #3746)
Pierre Letouzey
2015-12-22
*
Flag -compat 8.4 now loads Coq.Compat.Coq84.
Maxime Dénès
2015-12-14
*
Print Assumptions: improve detection of case on an axiom of False
Enrico Tassi
2015-12-09
*
Univs/Program: update the universe context with global universe
Matthieu Sozeau
2015-12-02
*
Fix bug #4444: Next Obligation performed after a Section opening was
Matthieu Sozeau
2015-12-02
*
Univs: correctly register universe binders for lemmas.
Matthieu Sozeau
2015-11-28
*
Fix [Polymorphic Hint Rewrite].
Matthieu Sozeau
2015-11-27
*
Univs: carry on universe substitution when defining obligations of
Matthieu Sozeau
2015-11-24
*
Fix output of universe arcs. (Fix bug #4422)
Guillaume Melquiond
2015-11-23
*
Univs: generation of induction schemes should not generated useless
Matthieu Sozeau
2015-11-20
*
Allow program hooks to see the refined universe_context at the end of a
Matthieu Sozeau
2015-11-19
*
Adding syntax "Show id" to show goal named id (shelved or not).
Hugo Herbelin
2015-11-02
*
Command.declare_definition: grab the fix_exn early (follows 77cf18e)
Enrico Tassi
2015-10-30
*
Add a way to get the right fix_exn in external vernacular commands
Matthieu Sozeau
2015-10-30
*
Accept option -compat 8.5. (Fix bug #4393)
Guillaume Melquiond
2015-10-29
*
Univs: local names handling.
Matthieu Sozeau
2015-10-28
*
Avoid type checking private_constants (side_eff) again during Qed (#4357).
Enrico Tassi
2015-10-28
*
Univs: fix bug #4375, accept universe binders on (co)-fixpoints
Matthieu Sozeau
2015-10-28
*
Fix bugs 4389, 4390 and 4391 due to wrong handling of universe names
Matthieu Sozeau
2015-10-27
*
Minor module cleanup : error HigherOrderInclude was never happening
Pierre Letouzey
2015-10-25
*
Miscellaneous typos, spacing, US spelling in comments or variable names.
Hugo Herbelin
2015-10-18
[next]