Jason Gross

`tmUnquote` (or `tmDefinition`) fails to propagate universe constraints

2

```coq From MetaCoq.Utils Require Import utils MCList. From MetaCoq.Template Require Import MonadBasicAst MonadAst TemplateMonad Ast Loader. Require Import Equations.Prop.Classes. Require Import Coq.Lists.List. Import ListNotations. Local Set Primitive Projections. Local Open...

I'd like to be able to script adding definitions in submodules of the current module

```coq From MetaCoq.Utils Require Import bytestring. From MetaCoq.Template Require Import Loader TemplateMonad. From Coq Require Import MSetInterface MSetFacts. Open Scope bs. Locate Module Nop. (* Module Type Coq.Structures.Equalities.Nop *) MetaCoq...

I'd like to be able to generate new fresh universes, as well as add constraints between universes to the global environment directly from a `ConstraintSet.t`

`run_template_program (@tmQuote) (fun v => pose v).` tells me `tmQuote` takes 3 arguments (it only takes 2) `run_template_program (@tmQuoteModule) (fun v => pose v).` tells me `tmQuoteModule` takes 0 argument...

I want a variant of `tmCurrentModPath` that returns only the prefix of the current modpath which does not contain any functors. This is necessary for writing automation that tries to...

See https://github.com/MetaCoq/metacoq/pull/789#discussion_r1041398055

```coq (* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "+implicit-core-hint-db,+implicits-in-term,+non-reversible-notation,+deprecated-intros-until-0,+deprecated-focus,+unused-intro-pattern,+deprecated-hint-constr,+fragile-hint-constr,+variable-collision,+unexpected-implicit-declaration,+omega-is-deprecated,+deprecated-instantiate-syntax,+non-recursive,+deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,+undeclared-scope,+deprecated-typeclasses-transparency-without-locality,+future-coercion-class-field" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-R" "theories" "MetaCoq.Lob" "-top" "MetaCoq.Lob.Template.QuoteGround.Coq.MSets" "-native-compiler" "ondemand") -*- *) (* File reduced by coq-bug-minimizer from original input, then from...

metacoq/translations/times_bool_fun2.v is incompatible with the native compiler (Anomaly "Uncaught exception UGraph.UniverseInconsistency(_).")

2

With Coq 8.16.0, Equations tag v1.3-8.16, metacoq at the tip of coq-8.16 (d702f18ce289530cdd0be3d0ad331cb1ad38f6a0), when coq-native has been installed, the build fails with ``` COQNATIVE times_bool_fun2.vo Error: Anomaly "Uncaught exception UGraph.UniverseInconsistency(_)."...