index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
kernel
/
declarations.ml
Age
Commit message (
Expand
)
Author
2020-07-06
Primitive persistent arrays
Maxime Dénès
2020-07-01
UIP in SProp
Gaëtan Gilbert
2020-04-30
Merge PR #12107: Remove mod_constraints field of module body
Pierre-Marie Pédrot
2020-04-20
Remove mod_constraints field of module body
Gaëtan Gilbert
2020-04-16
Make cumulative sprop a typing flag, deprecate command line -sprop-cumulative
Gaëtan Gilbert
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2020-03-08
Ensure that template parameters are shared in the same inductive block.
Pierre-Marie Pédrot
2020-02-09
Remove the Template Check option.
Pierre-Marie Pédrot
2020-02-05
Store the template polymorphic context inside the TemplateArity node.
Pierre-Marie Pédrot
2020-01-15
Discharge inductive types without rechecking them
Gaëtan Gilbert
2020-01-15
generate variance data for section universes (not yet used)
Gaëtan Gilbert
2019-11-21
[coq] Untabify the whole ML codebase.
Emilio Jesus Gallego Arias
2019-08-26
Make kernel parametric on the lowest universe and fix #9294
Matthieu Sozeau
2019-08-16
Split the [check_guarded] typing_flag into [check_guarded] (for (co)fixpoints...
SimonBoulier
2019-06-17
Merge PR #10362: Kernel-side delaying of polymorphic opaque constants
Gaëtan Gilbert
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-06-17
Allow to delay polymorphic opaque constants.
Pierre-Marie Pédrot
2019-05-27
mind_kelim is the highest allowed sort instead of a list
Gaëtan Gilbert
2019-05-23
Fixing typos - Part 2
JPR
2019-05-19
Parameterize the constant_body type by opaque subproofs.
Pierre-Marie Pédrot
2019-05-19
Make the type of constant bodies parametric on opaque proofs.
Pierre-Marie Pédrot
2019-03-14
Repair relevance marks in-kernel.
Gaëtan Gilbert
2019-03-14
Add relevance marks on binders.
Gaëtan Gilbert
2019-02-28
Constructor type information uses the expanded form.
Pierre-Marie Pédrot
2019-02-17
Separate variance and universe fields in inductives.
Gaëtan Gilbert
2019-02-04
Primitive integers
Maxime Dénès
2018-11-27
Merge PR #8850: Private universes for opaque polymorphic constants.
Matthieu Sozeau
2018-11-26
Put -indices-matter in typing_flags
Gaëtan Gilbert
2018-11-23
Local universes for opaque polymorphic constants.
Gaëtan Gilbert
2018-11-05
Pass native and VM flags to the kernel through environment
Maxime Dénès
2018-09-17
[VM] Move structured_constant to Vmvalues
Maxime Dénès
2018-07-26
Turn the kernel reduction sharing flag into an argument passed in the cache.
Pierre-Marie Pédrot
2018-07-24
Projections use index representation
Gaëtan Gilbert
2018-06-27
Swapping Context and Constr: defining declarations on constr in Constr.
Hugo Herbelin
2018-06-23
Using more general information for primitive records.
Pierre-Marie Pédrot
2018-06-23
Change the proj_ind field from MutInd.t to inductive.
Pierre-Marie Pédrot
2018-06-17
Remove the proj_body field from the kernel.
Pierre-Marie Pédrot
2018-06-17
Remove the proj_eta field of the kernel.
Pierre-Marie Pédrot
2018-06-17
Getting rid of the const_proj field in the kernel.
Pierre-Marie Pédrot
2018-06-05
Use projection indices in native compilation rather than constant names.
Pierre-Marie Pédrot
2018-05-31
Reduce circular dependency constants <-> projections
Gaëtan Gilbert
2018-02-27
Update headers following #6543.
Théo Zimmermann
2018-02-16
Extrude monomorphic universe contexts from with Definition constraints.
Pierre-Marie Pédrot
2018-01-14
Store the conversion oracle in constant and inductive definitions.
Pierre-Marie Pédrot
2017-12-10
[api] Remove kernel dependency on intf (Decl_kind)
Emilio Jesus Gallego Arias
2017-11-24
When declaring constants/inductives use ContextSet if monomorphic.
Gaëtan Gilbert
2017-11-06
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
[api] Deprecate all legacy uses of Names in core.
Emilio Jesus Gallego Arias
2017-08-29
Statically enforcing that module types have no retroknowledge.
Pierre-Marie Pédrot
2017-08-29
Separating the module_type and module_body types by using a type parameter.
Pierre-Marie Pédrot
[next]
