index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
context.mli
Commit message (
Expand
)
Author
Age
*
Update headers following #6543.
Théo Zimmermann
2018-02-27
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
correcting comments in the "Context" module
Matej Kosik
2017-04-20
*
Introducing contexts parameterized by the inner term type.
Pierre-Marie Pédrot
2017-02-14
*
CLEANUP: adding "Context.Compacted.Declaration.of_named_decl" function, which...
Matej Kosik
2016-08-26
*
CLEANUP: rename "Context.Named.{to,of}_rel" functions to "Context.Named.{to,o...
Matej Kosik
2016-08-26
*
CLEANUP: renaming "Context.ListNamed" module to "Context.Compacted"
Matej Kosik
2016-08-26
*
CLEANUP: changing the definition of the "Context.NamedList.Declaration" type
Matej Kosik
2016-08-25
*
CLEANUP: Type alias "Context.section_context" was removed
Matej Kosik
2016-08-25
*
CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to "Contex...
Matej Kosik
2016-08-25
*
Merging a branch that adds "Context.Named.Declaration.to_rel" function.
Matej Kosik
2016-08-24
|
\
|
*
Adding "Context.Named.Declaration.to_rel" function
Matej Kosik
2016-08-24
*
|
Revert "CLEANUP: removing the definition of the "Context.Rel.Declaration.to_t...
Pierre-Marie Pédrot
2016-08-17
|
/
*
Adding "Context.Named.Declaraton.of_rel" function
Matej Kosik
2016-08-11
*
CLEANUP: removing the definition of the "Context.Rel.Declaration.of_tuple" fu...
Matej Kosik
2016-08-11
*
CLEANUP: removing the definition of the "Context.Rel.Declaration.to_tuple" fu...
Matej Kosik
2016-08-11
*
REFORMATTING: kernel/context.ml{,i}
Matej Kosik
2016-02-09
*
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-11
*
|
Moving extended_rel_vect/extended_rel_list to the kernel.
Hugo Herbelin
2015-12-05
|
/
*
Update headers.
Maxime Dénès
2015-01-12
*
Pushing Pierre's factorization of names in goal context printing from
Hugo Herbelin
2014-10-22
*
A patch for printing "match" when constructors are defined with let-in
Hugo Herbelin
2014-10-20
*
Coqide prints succesive hyps of the same type on 1 line
Pierre Boutillier
2014-09-01
*
Removing some generic equalities.
ppedrot
2013-10-22
*
Removing useless casts between arrays and lists.
ppedrot
2013-08-04
*
Merging Context and Sign.
ppedrot
2013-04-29
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29