index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
indtypes.ml
Commit message (
Expand
)
Author
Age
...
*
|
|
Merge origin/v8.5 into trunk
Hugo Herbelin
2015-11-10
|
\
|
|
|
*
|
Dead code from the commit having introduced primitive projections (a4043608).
Hugo Herbelin
2015-11-10
|
*
|
Fixing a bug in reporting ill-formed constructor.
Hugo Herbelin
2015-11-10
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-26
|
\
|
|
|
*
|
Fixing a bug in reporting ill-formed inductive.
Hugo Herbelin
2015-10-22
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-15
|
\
|
|
|
*
|
Univs: inductives, remove unneeded test
Matthieu Sozeau
2015-10-14
*
|
|
Splitting kernel universe code in two modules.
Pierre-Marie Pédrot
2015-10-06
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-02
|
\
|
|
|
*
|
Universes: enforce Set <= i for all Type occurrences.
Matthieu Sozeau
2015-10-02
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-09-06
|
\
|
|
|
*
|
Implementing Herbelin's fix for the "NonPar" bug
mlasson
2015-09-03
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-07-18
|
\
|
|
|
*
|
Option -type-in-type: added support in checker and making it contaminating
Hugo Herbelin
2015-07-10
|
*
|
Kernel: primitive projections handling of let-ins
Matthieu Sozeau
2015-07-09
|
*
|
Template polymorphism: A bug-fix for Bug #4258
mlasson
2015-07-09
|
|
*
Add a corresponding field in `mutual_inductive_entry` (part 2).
Arnaud Spiwack
2015-06-24
|
|
*
Add a corresponding field in `mutual_inductive_entry` (part 1).
Arnaud Spiwack
2015-06-24
|
|
*
Add a field in `mutual_inductive_body` to represent mutual inductive whose po...
Arnaud Spiwack
2015-06-24
|
|
/
|
/
|
*
|
Document the positivity checker.
Arnaud Spiwack
2015-06-23
|
/
*
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
*
Univs: When computing the level of an inductive including indices, lets
Matthieu Sozeau
2015-02-14
*
Removing dead code.
Pierre-Marie Pédrot
2015-02-02
*
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
*
kernel/ind Change interface of declare_mind and declare_mutual
Matthieu Sozeau
2015-01-05
*
Fix treatment of universe context in typecheck inductive (was added
Matthieu Sozeau
2014-12-15
*
Pass around information on the use of template polymorphism for
Matthieu Sozeau
2014-11-23
*
Option -type-in-type continued (deactivate test for inferred sort of
Hugo Herbelin
2014-11-19
*
A patch for printing "match" when constructors are defined with let-in
Hugo Herbelin
2014-10-20
*
Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name
Matthieu Sozeau
2014-10-11
*
Add a boolean to indicate the unfolding state of a primitive projection,
Matthieu Sozeau
2014-09-27
*
Fix generation of inductive elimination principle for primitive records.
Matthieu Sozeau
2014-09-10
*
Fix primitive projections declarations for inductive records.
Matthieu Sozeau
2014-09-05
*
Simplify even further the declaration of primitive projections,
Matthieu Sozeau
2014-08-30
*
Add test-suite file. Compute the name for the record binder in the
Matthieu Sozeau
2014-08-29
*
Change the way primitive projections are declared to the kernel.
Matthieu Sozeau
2014-08-28
*
"allows to", like "allowing to", is improper
Jason Gross
2014-08-25
*
Move to a representation of universe polymorphic constants using indices for ...
Matthieu Sozeau
2014-08-03
*
A tentative uniform naming policy in module Inductiveops.
Hugo Herbelin
2014-08-01
*
- Do module substitution inside mind_record.
Matthieu Sozeau
2014-07-25
*
Refining match subterm and commutative cut rules. The parameters that are
Maxime Dénès
2014-07-22
*
Properly add a Set lower bound on any polymorphic inductive in Type with
Matthieu Sozeau
2014-07-11
*
Cleanup code related to the constraint solving, which sits now outside the
Matthieu Sozeau
2014-07-03
*
Fix computation of inductive level in monomorphism + indices-matter mode.
Matthieu Sozeau
2014-06-20
*
Fix a destArity that does not exactly match isArity in presence of let-ins.
Matthieu Sozeau
2014-06-17
*
Removing dead code.
Pierre-Marie Pédrot
2014-06-17
*
Reuse universe level substitutions for template polymorphism, fixing performance
Matthieu Sozeau
2014-05-09
*
- Fix bug preventing apply from unfolding Fixpoints.
Matthieu Sozeau
2014-05-06
[prev]
[next]