Abhishek Anand

this works when I jump to definition for a definition/inductive etc. However, it doesnt work when I jump to definition on a line of the form "Require Import x.y.z". It...

i just created that branch, which currently points to 75127a6

`tmDependencies` was almost definable in the monad (even before this PR)? Fuel was needed to circumvent the issue of convincing the termination checker. Would it be better (more general) to...

When used, the option of making fixpoints unguarded will make the entire logic inconsistent. Adding a fixpoint combinator to the monad will not. -- Abhishek http://www.cs.cornell.edu/~aa755/ On Wed, May 8,...

The proof is on paper only, although I had [sketched](https://github.com/aa755/paramcoq-iff/blob/coq-8.6/proof.v) in Coq some cases of the lemma that says that substitution commutes with the translation. The Coq sketch was just...

I'd like to see an example of a use of `Prop` that cannot be accomplished with just the `erased` type constructor. Like Props, erased types have proof irrelevance. For example,...

1) `erased` can ~~should~~ be defined in a way such that proof irrelevance is consistent or even provable for erased types. ~~I don't know how `opaque` works, but it does...

Right. Putting anything sensible for `reveal` seems to contradict proof relevance. Sorry, it had nothing to do with `opaque`. We can still have `hide` and `emap (('a->'b) -> erased 'a...

A problem with the Prop universe approach that once one defines something, e.g. inductively defined proposition, in the Prop universe, there is no way to use it in a constructive...

I don't know if it is possible to be polymorphic over both `Prop` and `Type_i`, i.e., to quantify a variable, say `T`, in a way that it can be instantiated...