aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/search.ml
Commit message (Collapse)AuthorAge
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
| | | | | | | | | | | | | In #6092, `global_reference` was moved to `kernel`. It makes sense to go further and use the current kernel style for names. This has a good effect on the dependency graph, as some core modules don't depend on library anymore. A question about providing equality for the GloRef module remains, as there are two different notions of equality for constants. In that sense, `KerPair` seems suspicious and at some point it should be looked at.
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
| | | | We do up to `Term` which is the main bulk of the changes.
* Remove the function Global.type_of_global_unsafe.Gravatar Pierre-Marie Pédrot2017-07-13
|
* Getting rid of AUContext abstraction breakers in Search.Gravatar Pierre-Marie Pédrot2017-07-13
|
* Safe API for accessing universe constraints of global references.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | | | Instead of returning either an instance or the set of constraints, we rather return the corresponding abstracted context. We also push back all uses of abstraction-breaking calls from these functions out of the kernel.
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
|
* Remove (useless) aliases from the API.Gravatar Matej Košík2017-06-10
|
* [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
| | | | | | | | | | | | Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which this PR solves, I propose to remove support for non-synchronous options. It seems the few uses of `optsync = false` we legacy and shouldn't have any impact. Moreover, non synchronous options may create particularly tricky situations as for instance, they won't be propagated to workers.
* Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
|
* Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
|
* [pp] Remove uses of expensive string_of_ppcmds.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | In general we want to avoid this as much as we can, as it will need to make choices regarding the output backend (width, etc...) and it is expensive. It is better to serve the printing backends the pretty print document itself.
* [stm] Break stm/toplevel dependency loop.Gravatar Emilio Jesus Gallego Arias2017-02-15
Currently, the STM, vernac interpretation, and the toplevel are intertwined in a mutual dependency that needs to be resolved using imperative callbacks. This is problematic for a few reasons, in particular it makes the interpretation of commands that affect the document quite intricate. As a first step, we split the `toplevel/` directory into two: "pure" vernac interpretation is moved to the `vernac/` directory, on which the STM relies. Test suite passes, and only one command seems to be disabled with this approach, "Show Script" which is to my understanding obsolete. Subsequent commits will fix this and refine some of the invariants that are not needed anymore.