index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
Commit message (
Expand
)
Author
Age
*
Fix some typos.
Guillaume Melquiond
2015-10-13
*
Univs: be more restrictive for template polymorphic constants: only
Matthieu Sozeau
2015-10-12
*
Gather VM tags in Cbytecodes.
Maxime Dénès
2015-10-12
*
Complete handling of primitive projections in VM.
Maxime Dénès
2015-10-09
*
Code cleaning in VM (with Benjamin).
Maxime Dénès
2015-10-09
*
Univs: fix bug #3807
Matthieu Sozeau
2015-10-08
*
Proof using: let-in policy, optional auto-clear, forward closure*
Enrico Tassi
2015-10-08
*
term_typing: strengthen discharging code
Enrico Tassi
2015-10-08
*
Univs: fix bug #4288, Print Sorted generated backward < constraints.
Matthieu Sozeau
2015-10-05
*
Univs: Change intf of push_named_def to return the computed universe
Matthieu Sozeau
2015-10-02
*
Univs: refined handling of assumptions
Matthieu Sozeau
2015-10-02
*
Univs: forgot a substitution in mod_typing.
Matthieu Sozeau
2015-10-02
*
Univs: correct handling of with in modules
Matthieu Sozeau
2015-10-02
*
Univs: fix bug #4251, handling of template polymorphic constants.
Matthieu Sozeau
2015-10-02
*
Univs: fix subtyping of polymorphic parameters.
Matthieu Sozeau
2015-10-02
*
Univs: uncovered bug in strengthening of opaque polymorphic definitions.
Matthieu Sozeau
2015-10-02
*
Univs: handle side-effects of futures correctly in kernel.
Matthieu Sozeau
2015-10-02
*
Univs (kernel) adapt to new invariants
Matthieu Sozeau
2015-10-02
*
Univs: module constraints move to universe contexts as they might
Matthieu Sozeau
2015-10-02
*
Forcing i > Set for global universes (incomplete)
Matthieu Sozeau
2015-10-02
*
Universes: enforce Set <= i for all Type occurrences.
Matthieu Sozeau
2015-10-02
*
Remove unused type_in_type field in safe_env.
Maxime Dénès
2015-09-20
*
Fix #3948 Anomaly: unknown constant in Print Assumptions
Maxime Dénès
2015-09-20
*
Fix a bug in 31 bit arithmetic, leading to failing conversion tests.
Maxime Dénès
2015-09-06
*
Fixed critical bug in 31 bit arithmetic of VM
Catalin Hritcu
2015-09-06
*
print universes when dumping bytecode.
Gregory Malecha
2015-09-03
*
Implementing Herbelin's fix for the "NonPar" bug
mlasson
2015-09-03
*
Fixing pop_rel_context.
Hugo Herbelin
2015-08-02
*
Reverting 16 last commits, committed mistakenly using the wrong push command.
Hugo Herbelin
2015-08-02
*
Fixing pop_rel_context
Hugo Herbelin
2015-08-02
*
A patch renaming equal into eq in the module dealing with
Hugo Herbelin
2015-08-02
*
Adding eq/compare/hash for syntactic view at
Hugo Herbelin
2015-08-02
*
Followup of 9f81b58551.
Pierre-Marie Pédrot
2015-07-30
*
Fixing bug #4289 (hash-consing only user part of constant not
Hugo Herbelin
2015-07-30
*
Fixing some English misspelling.
Hugo Herbelin
2015-07-29
*
a small amount of documentation on the virtual machine.
Gregory Malecha
2015-07-23
*
Fix incomplete pattern-matching.
Matthieu Sozeau
2015-07-22
*
Modules: fix bug #4294
Matthieu Sozeau
2015-07-16
*
Univs/Inductive: fix typechecking of cases
Matthieu Sozeau
2015-07-15
*
Unused variables reported by OCaml.
Hugo Herbelin
2015-07-10
*
Option -type-in-type: added support in checker and making it contaminating
Hugo Herbelin
2015-07-10
*
Native compiler: make non-fatal linking errors silent except in debug mode.
Maxime Dénès
2015-07-10
*
Native compiler: refactor code handling pre-computed values.
Maxime Dénès
2015-07-10
*
Kernel/Checker: Cleanup fixes of substitutions due to let-ins.
Matthieu Sozeau
2015-07-09
*
Kernel: primitive projections handling of let-ins
Matthieu Sozeau
2015-07-09
*
Improve semantics of -native-compiler flag.
Maxime Dénès
2015-07-09
*
Template polymorphism: A bug-fix for Bug #4258
mlasson
2015-07-09
*
Univs: bug fix.
Matthieu Sozeau
2015-07-07
*
Fixing documentation (see Maxime's mail on coqdev, July 3).
Hugo Herbelin
2015-07-05
*
Fix handling of primitive projections in VM.
Maxime Dénès
2015-07-05
[next]