Gregory Malecha

Thanks. I was having trouble with `vinyl` in my setup for some reason and `union` also uses it. The strictness annotations are a good point though. Even with that, `Data.Union`...

This was also suggested in https://github.com/MetaCoq/metacoq/pull/133

An alternative is to make the definition coinductive, which would also work and might make it possible to prove termination after the fact using existing Coq mechanisms.

Yes. The original motivation was exactly that, I was thinking that you could play tricks with partially applied functions, but that breaks Coq's internal invariants. It isn't important to do...

You probably want to phrase a `viewApp : term -> term * list term` that would guarantee that the resulting term does not have a head `tApp` constructor.

Personally, I think targeting PCUIC is the righy way to go, at least at the level that I understand things.

Just as a note, the `term` generated is the following: ```coq (tApp (tConstruct {| inductive_mind := "Coq.Init.Logic.and"; inductive_ind := 0 |} 0 nil) (tInd {| inductive_mind := "meta.TT"; inductive_ind :=...

Sketch in #131. Is there a test suite for `translations/translation_utils.v`? @mattam82 @SimonBoulier

Thanks! I started looking into porting the uses of `translation_utils.v` this morning and ran into the following. ```coq Definition bool_TC : tsl_context. run_template_program (Translate emptyTC "Coq.Init.Datatypes.bool") ltac:(fun tc => let...

Possibly relevant. The output after running the tactic is: ```coq Translate Coq.Init.Datatypes.bool boolᵗ is defined boolᵗ_rect is defined boolᵗ_ind is defined boolᵗ_rec is defined Coq.Init.Datatypes.bool has been translated. ``` And...