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 ill-typed debugging code in the VM.
Guillaume Melquiond
2015-04-27
*
Tactical `progress` compares term up to potentially equalisable universes.
Arnaud Spiwack
2015-04-22
*
Fixing bug #4190.
Pierre-Marie Pédrot
2015-04-16
*
fix code and bound for SWITCH instruction.
Benjamin Gregoire
2015-03-30
*
use a more compact representation of non-constant constructors
Benjamin Gregoire
2015-03-27
*
allows the vm to deal with inductive type with 8388607 constant constructors ...
Benjamin Gregoire
2015-03-26
*
Fix bug 4157,
Benjamin Gregoire
2015-03-26
*
Fix vm compiler to refuse to compile code making use of inductives with
Matthieu Sozeau
2015-03-25
*
More clever representation of substituted Cemitcode.
Pierre-Marie Pédrot
2015-03-25
*
Fully fixing bug #3491 (anomaly when building _rect scheme in the
Hugo Herbelin
2015-03-25
*
Fixing computation of non-recursively uniform arguments in the
Hugo Herbelin
2015-03-24
*
Fixing wrong rel_context in checking positivity condition.
Hugo Herbelin
2015-03-24
*
More sharing in module substitution.
Pierre-Marie Pédrot
2015-03-18
*
Fix compilation with forthcoming Ocaml version 4.03.
Arnaud Spiwack
2015-03-13
*
Fix bug #4103: forgot to allow unfolding projections of cofixpoints like
Matthieu Sozeau
2015-03-03
*
Add support so that the type of a match in an inductive type with let-in
Hugo Herbelin
2015-02-27
*
New function [Constr.equal_with] to compare terms up to variants of [kind_of_...
Arnaud Spiwack
2015-02-24
*
Refactoring in [Constr].
Arnaud Spiwack
2015-02-24
*
Fix some typos in comments.
Guillaume Melquiond
2015-02-23
*
Import (module): Do not force constraints if not ready (Close #4066)
Enrico Tassi
2015-02-21
*
Univs: When computing the level of an inductive including indices, lets
Matthieu Sozeau
2015-02-14
*
Univs: fix bug #3978: carry around the universe context used to
Matthieu Sozeau
2015-02-12
*
Fixing bug #4019, and checker blow-up at once.
Pierre-Marie Pédrot
2015-02-11
*
Clarifying the implementation of universe hashconsing.
Pierre-Marie Pédrot
2015-02-11
*
Fix typeops ignoring results of check functions with let _, and one
Matthieu Sozeau
2015-02-10
*
Nativelib: catch Unix_error (like no ocamlopt found)
Enrico Tassi
2015-02-04
*
Removing dead code.
Pierre-Marie Pédrot
2015-02-02
*
Fixing bug #3931.
Pierre-Marie Pédrot
2015-01-28
*
Fix a critical bug in machine arithmetic for native compiler.
Maxime Dénès
2015-01-20
*
Fix #3379, now that Require inside modules is allowed again.
Maxime Dénès
2015-01-17
*
Univs: proper printing of global and local universe names (only
Matthieu Sozeau
2015-01-17
*
Partially revert "Forbid Require inside interactive modules and module types."
Maxime Dénès
2015-01-17
*
Univs: Fix alias computation for VMs, computation of normal form of
Matthieu Sozeau
2015-01-17
*
Make native compiler handle universe polymorphic definitions.
Maxime Dénès
2015-01-17
*
Correct restriction of vm_compute when handling universe polymorphic
Matthieu Sozeau
2015-01-15
*
Make -print-mod-uid accept a list of files.
Maxime Dénès
2015-01-15
*
Native compiler: if debug flag not present, remove .native files.
Maxime Dénès
2015-01-13
*
Fix bug when discharging universe constraints coming from variables
Matthieu Sozeau
2015-01-13
*
Fix issue in printing due to de Bruijn bug when constructing compatibility
Matthieu Sozeau
2015-01-13
*
Update headers.
Maxime Dénès
2015-01-12
*
Fix a few typos.
Maxime Dénès
2015-01-12
*
Declarations.mli refactoring: module_type_body = module_body
Pierre Letouzey
2015-01-11
*
Aligning printing of universe constraints.
Hugo Herbelin
2015-01-07
*
Fix some documentation typos.
Guillaume Melquiond
2015-01-06
*
improve efficiency of the reduction interpreter of coqtop
Bruno Barras
2015-01-06
*
Rename ill-named "imports" field of safe_env into "required".
Maxime Dénès
2015-01-06
*
kernel/ind Change interface of declare_mind and declare_mutual
Matthieu Sozeau
2015-01-05
*
universes_of_constant: do a proper set union of body and type univs
Enrico Tassi
2014-12-27
*
Revert "Term: include a function to print terms"
Enrico Tassi
2014-12-27
*
Term: include a function to print terms
Enrico Tassi
2014-12-26
[next]