Gregory Malecha
Gregory Malecha
This removes the dependency on vinyl which seems to have compilation errors with recent versions of GHC.
This is a proposal to implement `tmQuoteRecursive` using an action `tmDependencies` that returns a list of all of the dependencies. The client can then traverse the list to compute the...
One thing that makes terms quite large is the use of ascii strings. I released a very simple bytestring library (http://coq.io/opam/coq-bytestring.0.9.0.html) that would reduce the size of the strings that...
I wanted to experiment with the possibility of using template-coq as a tactic language to solve a "simple" problem with universes (which was the impetus for my initial question on...
Are there any examples of people using the template monad to generate universe polymorphic code? I was having difficulty generating polymorphic lenses in the lens library: https://github.com/gmalecha/coq-lens/blob/master/theories/Lens.v
I'm wondering if it would of interest to provide explicit sharing information in terms. I imagine something like: ```coq tTerm (nm : positive) (t : term) (_ : term) tRef...
Per discussion on the gitter. Coq trunk contains: ```ocaml (* coq trunk *) type import_status = ImportDefaultBehavior | ImportNeedQualified type locality = Discharge | Global of import_status (* coq <...
If it can't be done, then it would be good to understand why.
I just recently started looking into PCUIC and it looks really great. Would it be possible to replace the Template.Ast.term definition with this one? Are there features that exist in...
Most things in Structures should be universe polymorphic.