dependent-types

Originally proposed by @charguer as part of #10559 as:

• The command Open HintDb mybase. loads mybase over the current section/module, meaning that eauto implicitly means eauto with mybase.

~~I personally have my doubts on the Open HintDb syntax because I find it too close to the Open Scope command and therefore likely to make users think that its effects are cumulative (you coul

This is very low prio, but it usually happens that when touching Prims or some other file high in the dependency graph, we get spurious diffs in many other files. Since we check-in the snapshot, and we need to have it up-to-date, we get very verbose commits when nothing relevant changed. Plus, when something did change, it's hard to spot.

Example: I removed a few lines in prims and get things

Describe the bug

When installing the Kind toolchain the kind-scm command is installed. When I read [THEOREMS.md][theorems] the command is named kind.

To Reproduce

Steps to reproduce the behavior:

1. Following installation instructions for Ubuntu
2. Read [THEOREMS.md][theorems]

Expected behavior

I would expect

It would be a nice convenience to allow the syntax

import M as _.

This would have the effect of checking module M but not adding any of its names to the context of the importing file. The use case for this is if you want to have a single Cedille source file that includes a bunch of other files, without having to worry about namespace clashes. This would be handy for testing. One can achie