Code like

have {H}H : ...

triggers a cryptic warning. It should suggest to write

have {}H : ...

instead.

See also: https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/duplicate.20clear

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

A formula like forall x1. forall. x2. exists x3. phi gets resugared to, and hence pretty printed as, forall x1 x2 x3. phi. The bug is in the uncurry function in FStar.Syntax.Reguar.fs.

(spotted by locria)

Steps to Reproduce

f : (0 x : (a,b)) -> Nat
f x =
  let 0 (u,v) = x in
  0

Expected Behavior

Type-check fine, with 0 u : a and 0 v : b in scope inside the let body.

Observed Behavior

     While processing right hand side of f. x is not accessible in this
     context.
     
      09 | f : (0 x : (a,b)) -> Nat
      10 | f x =

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