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
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-03
|
\
|
*
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
*
|
Removing dead code in Obligations.
Pierre-Marie Pédrot
2015-12-02
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-29
|
\
|
|
*
Univs: correctly register universe binders for lemmas.
Matthieu Sozeau
2015-11-28
|
*
Fix [Polymorphic Hint Rewrite].
Matthieu Sozeau
2015-11-27
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-26
|
\
|
|
*
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
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-20
|
\
|
|
*
Allow program hooks to see the refined universe_context at the end of a
Matthieu Sozeau
2015-11-19
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-05
|
\
|
|
*
Adding syntax "Show id" to show goal named id (shelved or not).
Hugo Herbelin
2015-11-02
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-30
|
\
|
|
*
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
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-29
|
\
|
|
*
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
*
|
Type-safe Egramml.grammar_prod_item.
Pierre-Marie Pédrot
2015-10-27
*
|
Finer type for Pcoq.interp_entry_name.
Pierre-Marie Pédrot
2015-10-27
*
|
Indexing existentially quantified entries returned by interp_entry_name.
Pierre-Marie Pédrot
2015-10-27
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-26
|
\
|
|
*
Minor module cleanup : error HigherOrderInclude was never happening
Pierre Letouzey
2015-10-25
*
|
Pcoq.prod_entry_key now uses a GADT to statically enforce typedness.
Pierre-Marie Pédrot
2015-10-21
*
|
Boxing the Goal.enter primitive into a record type.
Pierre-Marie Pédrot
2015-10-20
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-19
|
\
|
*
|
Constraining refine to monotonic functions.
Pierre-Marie Pédrot
2015-10-18
|
*
Miscellaneous typos, spacing, US spelling in comments or variable names.
Hugo Herbelin
2015-10-18
*
|
Clarifying and documenting the UState API.
Pierre-Marie Pédrot
2015-10-17
|
*
Lemmas accept the Local flag.
Pierre-Marie Pédrot
2015-10-17
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-15
|
\
|
|
*
Remove -vm flag of coqtop.
Maxime Dénès
2015-10-14
|
*
Fixing bug #4367: Wrong error message in unification.
Pierre-Marie Pédrot
2015-10-14
|
*
Fix some typos.
Guillaume Melquiond
2015-10-13
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-12
|
\
|
|
*
Fix Definition id := Eval <redexpr> in by passing the right universe
Matthieu Sozeau
2015-10-12
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-10
|
\
|
|
*
Code cleaning in VM (with Benjamin).
Maxime Dénès
2015-10-09
|
*
Fix Next Obligation to not raise an anomaly in case of mutual
Matthieu Sozeau
2015-10-09
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-09
|
\
|
|
*
Axioms now support the universe binding syntax.
Pierre-Marie Pédrot
2015-10-08
|
*
aux_file: export API to ease writing of a Proof Using annotator.
Enrico Tassi
2015-10-08
|
*
Proof using: let-in policy, optional auto-clear, forward closure*
Enrico Tassi
2015-10-08
|
*
Spawn: use each socket exclusively for writing or reading
Enrico Tassi
2015-10-08
[next]