Jason Gross

Or, at least, in refreshing the universes at each occurance. -Jason On Jun 23, 2014 11:22 AM, "Jason Gross" [email protected] wrote: > I would be in favor of retypechecking c...

Why does `present_obj` force `C` and `D` to be at the same level? Is it possible to see the local universe graph in the middle of a proof? Also, would...

I think my preferred default semantics for `change` are "introduce fresh universes wherever needed, and equate as needed afterwards". Perhaps `change ` should not do this, and `change ... with...

(My general motto being "I shouldn't have to think about universes unless I'm being evil; otherwise, they should just work, as generally as possible, unless making them just work is...

This will still unify universes though, right? For example, if I have `Contr_internal` showing up in a bunch of places at various universe levels, and I do `change Contr_internal with...

`change` seems broken in trunk (https://coq.inria.fr/bugs/show_bug.cgi?id=3387): ``` coq Goal Type@{i} = Type@{j}. Proof. (* 1 subgoals , subgoal 1 (ID 3) ============================ Type@{Top.368} = Type@{Top.370} (dependent evars:) *) let x...

Oops, I forgot the forall instance that made it compile in HoTT/coq, which I've now put back. This might be a "the unification engine changed, it's not getting fixed" bug....

If you're talking about the fact that `point A` meant `@point _ _ A`, yes, that's weird. Does the revised test case trigger the error in the old code, though?...

Current trunk (90d64647d3fd5dbf5c337944dc0038f0b19b8a51) gives the error on the original code. Older versions of Coq inferred that I was asking for a point of the type `(forall x : Type, (fun...

I bet this is because you don't know at tactic time whether the current definition is monomorphic or polymorphic, and in the polymorphic case, you don't add them to the...