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
*
Primitive projections: protect kernel from erroneous definitions.
Matthieu Sozeau
2016-03-10
*
Fixing bde12b70 about reporting ill-formed constructor.
Hugo Herbelin
2016-01-26
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Fixing fix c71aa6b to primitive projections.
Hugo Herbelin
2015-11-18
*
Slightly documenting code for building primitive projections.
Hugo Herbelin
2015-11-18
*
Fixing logical bugs in the presence of let-ins in computiong primitive
Hugo Herbelin
2015-11-18
*
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
*
Fixing a bug in reporting ill-formed inductive.
Hugo Herbelin
2015-10-22
*
Univs: inductives, remove unneeded test
Matthieu Sozeau
2015-10-14
*
Universes: enforce Set <= i for all Type occurrences.
Matthieu Sozeau
2015-10-02
*
Implementing Herbelin's fix for the "NonPar" bug
mlasson
2015-09-03
*
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
*
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
*
Adapt Y. Bertot's path on private inductives (now the keyword is "Private").
Yves Bertot
2014-05-06
*
Initial work on reintroducing old-style polymorphism for compatibility (the s...
Matthieu Sozeau
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to
Hugo Herbelin
2014-04-28
*
Removing native_name reference from constant_body.
Maxime Dénès
2013-12-28
[next]