aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/context.ml
Commit message (Expand)AuthorAge
* Collecting List.smart_* functions into a module List.Smart.Gravatar Hugo Herbelin2018-05-23
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* A missing newline after a comment.Gravatar Hugo Herbelin2017-10-24
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Introducing contexts parameterized by the inner term type.Gravatar Pierre-Marie Pédrot2017-02-14
* CLEANUP: adding "Context.Compacted.Declaration.of_named_decl" function, which...Gravatar Matej Kosik2016-08-26
* CLEANUP: rename "Context.Named.{to,of}_rel" functions to "Context.Named.{to,o...Gravatar Matej Kosik2016-08-26
* CLEANUP: renaming "Context.ListNamed" module to "Context.Compacted"Gravatar Matej Kosik2016-08-26
* CLEANUP: changing the definition of the "Context.NamedList.Declaration" typeGravatar Matej Kosik2016-08-25
* CLEANUP: Type alias "Context.section_context" was removedGravatar Matej Kosik2016-08-25
* CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to "Contex...Gravatar Matej Kosik2016-08-25
* Merging a branch that adds "Context.Named.Declaration.to_rel" function.Gravatar Matej Kosik2016-08-24
|\
| * Adding "Context.Named.Declaration.to_rel" functionGravatar Matej Kosik2016-08-24
* | Revert "CLEANUP: removing the definition of the "Context.Rel.Declaration.to_t...Gravatar Pierre-Marie Pédrot2016-08-17
|/
* Adding "Context.Named.Declaraton.of_rel" functionGravatar Matej Kosik2016-08-11
* CLEANUP: removing the definition of the "Context.Rel.Declaration.of_tuple" fu...Gravatar Matej Kosik2016-08-11
* CLEANUP: removing the definition of the "Context.Rel.Declaration.to_tuple" fu...Gravatar Matej Kosik2016-08-11
* REFORMATTING: kernel/context.ml{,i}Gravatar Matej Kosik2016-02-09
* CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | Moving extended_rel_vect/extended_rel_list to the kernel.Gravatar Hugo Herbelin2015-12-05
|/
* Update headers.Gravatar Maxime Dénès2015-01-12
* Remove an ununsed pattern and commented code in the kernel.Gravatar Matthieu Sozeau2014-10-24
* Pushing Pierre's factorization of names in goal context printing fromGravatar Hugo Herbelin2014-10-22
* A patch for printing "match" when constructors are defined with let-inGravatar Hugo Herbelin2014-10-20
* Coqide prints succesive hyps of the same type on 1 lineGravatar Pierre Boutillier2014-09-01
* Removing some generic equalities.Gravatar ppedrot2013-10-22
* Removing useless casts between arrays and lists.Gravatar ppedrot2013-08-04
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-16 06:22:55 +0000