aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/evd.mli
Commit message (Collapse)AuthorAge
* Adding a bit of documentation in the mli.Gravatar Pierre-Marie Pédrot2016-06-09
|
* Allowing to attach location to universes in UState.Gravatar Pierre-Marie Pédrot2016-02-19
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-02-13
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|
* mergeGravatar Matej Kosik2016-01-11
|\
| * CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The structure of the Context module was refined in such a way that: - Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module. - Types and functions related to rel-context were put into the Context.Rel module. - Types and functions related to named-context declarations were put into the Context.Named.Declaration module. - Types and functions related to named-context were put into the Context.Named module. - Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module. - Types and functions related to named-list-context were put into Context.NamedList module. Some missing comments were added to the *.mli file. The output of ocamldoc was checked whether it looks in a reasonable way. "TODO: cleanup" was removed The order in which are exported functions listed in the *.mli file was changed. (as in a mature modules, this order usually is not random) The order of exported functions in Context.{Rel,Named} modules is now consistent. (as there is no special reason why that order should be different) The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file. (as there is no special reason to define them in a different order) The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do. (Now they are called Context.{Rel,Named}.fold_{inside,outside}) The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated. Thrown exceptions are now documented. Naming of formal parameters was made more consistent across different functions. Comments of similar functions in different modules are now consistent. Comments from *.mli files were copied to *.ml file. (We need that information in *.mli files because that is were ocamldoc needs it. It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function, we can see the comments also there and do not need to open a different file if we want to see it.) When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1. (UTF-8 characters are used in our ocamldoc markup) "open Context" was removed from all *.mli and *.ml files. (Originally, it was OK to do that. Now it is not.) An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed.
* | Remove duplicate declarations.Gravatar Guillaume Melquiond2016-01-01
|/
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-20
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-05
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-30
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-29
|
* Clarifying and documenting the UState API.Gravatar Pierre-Marie Pédrot2015-10-17
|
* Dedicated file for universe unification context manipulation.Gravatar Pierre-Marie Pédrot2015-10-17
| | | | | | | This allows to remove a lot of independent code from Evd which was put into the UState module. The API is not perfect yet, but this is a first pass. Names of data structures should be thought about too because they are way too similar.
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-09
|
* Splitting kernel universe code in two modules.Gravatar Pierre-Marie Pédrot2015-10-06
| | | | | 1. The Univ module now only cares about definitions about universes. 2. The UGraph module contains the algorithm responsible for aciclicity.
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|
* Removing meta_with_name from Evd.Gravatar Pierre-Marie Pédrot2015-09-27
|
* Removing subst_defined_metas_evars from Evd.Gravatar Pierre-Marie Pédrot2015-09-27
|
* Removing uselessly duplicated function in Evd.Gravatar Pierre-Marie Pédrot2015-09-27
|
* Hardening the API of evarmaps.Gravatar Pierre-Marie Pédrot2015-09-26
| | | | | | The evar counter has been moved from Evarutil to Evd, and all functions in Evarutil now go through a dedicated primitive to create a fresh evar from an evarmap.
* Merge branch 'v8.5' into trunkGravatar Maxime Dénès2015-09-17
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-06-01
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-05-05
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-03-23
|
* Adding a new folder corresponding to the low-level part of the pretyperGravatar Pierre-Marie Pédrot2015-02-27
together with the tactic monad. The move is not complete yet, because some file candidates for this directory have almost useless dependencies in other ones that should not be moved.