coq

coq copied to clipboard

Description of the problem

In particular it's not clear what the difference is between let x := f () in Control.refine (fun () => x) and Control.refine f. (And I don't know the answer to this.)

cc @ppedrot

Coq Version

8.16

Weird, I was pretty sure this used to be documented somewhere. The answer is that a thunk unit -> constr can create new evars, and those are added to the set of goals when refine returns. With the let-expanded function these evars are just shelved.