index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
checker
Commit message (
Expand
)
Author
Age
*
checker Indtypes: remove unused arguments
Gaëtan Gilbert
2018-07-03
*
checker Modops strengthening: remove unused argument resolver
Gaëtan Gilbert
2018-07-03
*
Subtyping.check_constant: remove unused module path argument.
Gaëtan Gilbert
2018-07-03
*
Inductive.extract_stack,filter_stack_domain: remove unused arguments
Gaëtan Gilbert
2018-07-03
*
Remove Sorts.contents
Gaëtan Gilbert
2018-06-26
*
Merge PR #7798: Remove hack skipping comparison of algebraic universes in sub...
Matthieu Sozeau
2018-06-25
|
\
*
|
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-23
|
*
Remove hack skipping comparison of algebraic universes in subtyping.
Gaëtan Gilbert
2018-06-22
|
*
Remove enforce_leq from checker
Gaëtan Gilbert
2018-06-21
|
/
*
Merge PR #7841: Remove Canary
Pierre-Marie Pédrot
2018-06-19
|
\
|
*
Remove Canary.
whitequark
2018-06-18
*
|
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-17
|
/
*
Fix the checker by merely adapting the data structure.
Pierre-Marie Pédrot
2018-06-07
*
Merge PR #7552: Fix #7539: Checker does not properly handle negative coinduct...
Matthieu Sozeau
2018-06-04
|
\
*
|
Reduce circular dependency constants <-> projections
Gaëtan Gilbert
2018-05-31
*
|
Merge PR #7325: Fix #7323: coqchk puts polymorphic univs of inductive in glob...
Pierre-Marie Pédrot
2018-05-25
|
\
\
*
\
\
Merge PR #7177: Unifying names of "smart" combinators + adding combinators in...
Pierre-Marie Pédrot
2018-05-24
|
\
\
\
|
|
*
|
Fix #7323: coqchk puts polymorphic univs of inductive in global env
Gaëtan Gilbert
2018-05-24
|
|
/
/
|
/
|
|
*
|
|
Merge PR #7328: Fix #7327: coqchk subtyping of polymorphic constants
Pierre-Marie Pédrot
2018-05-24
|
\
\
\
*
\
\
\
Merge PR #7317: Fix #6798: coqchk ignores ugraph when comparing constant inst...
Pierre-Marie Pédrot
2018-05-24
|
\
\
\
\
|
|
|
*
|
Moving Rtree.smart_map into Rtree.Smart.map.
Hugo Herbelin
2018-05-23
|
|
|
*
|
Moving Option.smart_map to Option.Smart.map.
Hugo Herbelin
2018-05-23
|
|
|
*
|
Collecting List.smart_* functions into a module List.Smart.
Hugo Herbelin
2018-05-23
|
|
|
*
|
Collecting Array.smart_* functions into a module Array.Smart.
Hugo Herbelin
2018-05-23
|
|
_
|
/
/
|
/
|
|
|
|
|
|
*
Fix #7539: Checker does not properly handle negative coinductive types.
Pierre-Marie Pédrot
2018-05-18
*
|
|
|
Infrastructure for ocamldebug on the checker
Gaëtan Gilbert
2018-05-13
|
|
_
|
/
|
/
|
|
|
|
*
Fix #7327: coqchk subtyping of polymorphic constants
Gaëtan Gilbert
2018-04-23
|
|
/
|
*
Fix #6798: coqchk ignores ugraph when comparing constant instances
Gaëtan Gilbert
2018-04-20
|
/
*
[api] Deprecate a couple of aliases that we missed.
Emilio Jesus Gallego Arias
2018-03-28
*
Merge PR #6800: [checker] Printer cleanup.
Maxime Dénès
2018-03-09
|
\
*
|
Update checker to reflect rule on constructors of polymorphic inductive types
Matthieu Sozeau
2018-03-08
|
*
[checker] Printer cleanup.
Emilio Jesus Gallego Arias
2018-03-07
|
/
*
Replace invalid tag @raises in ocamldoc comments with @raise
mrmr1993
2018-03-05
*
Merge PR #6855: Update headers following #6543.
Maxime Dénès
2018-03-05
|
\
*
\
Merge PR #6734: dest_{prod,lam}: no Cast case (it's removed by whd)
Maxime Dénès
2018-02-28
|
\
\
|
|
*
Update headers following #6543.
Théo Zimmermann
2018-02-27
|
|
/
|
/
|
*
|
Merge PR #6740: Adding a sanity check on inductive variance subtyping.
Maxime Dénès
2018-02-21
|
\
\
*
\
\
Merge PR #6728: Extrude monomorphic universe contexts from with Definition co...
Maxime Dénès
2018-02-19
|
\
\
\
*
\
\
\
Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ...
Maxime Dénès
2018-02-19
|
\
\
\
\
|
*
|
|
|
Change references to CAMLP4 to CAMLP5 to be more accurate since we no
Jim Fehrle
2018-02-17
|
|
*
|
|
Extrude monomorphic universe contexts from with Definition constraints.
Pierre-Marie Pédrot
2018-02-16
|
|
/
/
/
|
/
|
|
|
|
|
*
|
Adding a sanity check on inductive variance subtyping.
Pierre-Marie Pédrot
2018-02-15
|
|
/
/
|
/
|
|
*
|
|
Merge PR #6262: [error] Replace msg_error by a proper exception.
Maxime Dénès
2018-02-12
|
\
\
\
|
|
|
*
dest_{prod,lam}: no Cast case (it's removed by whd)
Gaëtan Gilbert
2018-02-11
|
|
|
/
*
|
/
Simplification: cumulativity information is variance information.
Gaëtan Gilbert
2018-02-10
|
|
/
|
/
|
|
*
[error] Replace msg_error by a proper exception.
Emilio Jesus Gallego Arias
2018-02-09
|
/
*
checker: cleanup projection unfolding
Gaëtan Gilbert
2018-02-02
[next]