Merge pull request #1188 from MetaRocq/fix-fresh-univ-ind

Fix handling of fresh_universes after tmMkInductive by restarting fro…

Author: mattam82

template-rocq/src/run_template_monad.ml

@@ -535,8 +535,9 @@ let rec run_template_program_rec ~poly ?(intactic=false) (k : Constr.t Plugin_co
     then not_in_tactic "tmMkInductive"
     else
       let infer_univs = unquote_bool (reduce_all env evm b) in
-      let evm = declare_inductive env evm infer_univs mind in
+      let _evm = declare_inductive env evm infer_univs mind in
       let env = Global.env () in
+      let evm = Evd.from_env env in
       k ~st env evm (Lazy.force unit_tt)
   | TmUnquote t ->
     begin
@@ -569,7 +570,7 @@ let rec run_template_program_rec ~poly ?(intactic=false) (k : Constr.t Plugin_co
        (* Typecheck. *)
        let evm = Typing.check env evm (EConstr.of_constr t') (EConstr.of_constr typ) in
        (* Solve evars. *)
-       let evm = Typeclasses.resolve_typeclasses env evm in 
+       let evm = Typeclasses.resolve_typeclasses env evm in
        let t' = Evarutil.nf_evars_universes evm t' in
        k ~st env evm t'
   | TmFreshName name ->

test-suite/_RocqProject.in

@@ -55,3 +55,5 @@ tmVariable.v
 unfold.v
 univ.v
 vs.v
+ind_fresh_univ.v
+

test-suite/ind_fresh_univ.v

@@ -0,0 +1,59 @@
+From MetaRocq.Utils Require Import utils.
+From MetaRocq.Template Require Import All.
+From MetaRocq.Template Require Import Checker.
+Import MRMonadNotation.
+
+(** MWE du bug sur les niveaux d'univers frais.*)
+
+Notation nameAnon := {| binder_name := nAnon; binder_relevance := Relevant |}.
+
+(* Inductive Ind (T : Type) : Prop :=. *)
+(* MetaRocq Run (tmQuote Ind >>= tmPrint). *)
+(* Modify this based on the current file. *)
+Definition ind : term :=
+  tInd {| inductive_mind := (MPfile ["ind_fresh_univ";"TestSuite";"MetaRocq"], "Ind") ; inductive_ind := 0 |} [].
+
+(* AST of [Inductive Ind (T : Type) : Prop :=.]. *)
+Definition AST_Ind := {|
+  ind_finite := Finite;
+  ind_npars := 1;
+  ind_params := [{|
+    decl_name := {| binder_name := nNamed "T"; binder_relevance := Relevant |};
+    decl_body := None;
+    decl_type := tSort (sType fresh_universe)
+  |}];
+  ind_bodies := [{|
+      ind_name := "Ind";
+      ind_indices := [];
+      ind_sort := sProp;
+      ind_type :=
+        tProd {| binder_name := nNamed "T"; binder_relevance := Relevant |}
+          (tSort (sType fresh_universe)) (tSort sProp);
+      ind_kelim := IntoPropSProp;
+      ind_ctors :=[];
+      ind_projs := [];
+      ind_relevance := Relevant
+    |}];
+  ind_universes := Monomorphic_ctx;
+  ind_variance := None
+|}.
+
+(* AST of [fun T : Type => Ind T]. *)
+Definition AST_fun :=
+  tLambda
+    {| binder_name := nNamed "T"; binder_relevance := Relevant |}
+    (tSort (sType fresh_universe))
+    (tApp ind [tRel 0]).
+
+Definition define_ind : TemplateMonad unit :=
+ tmMkInductive true (mind_body_to_entry AST_Ind).
+
+Definition define_fun : TemplateMonad unit :=
+  tmMkDefinition "def" AST_fun.
+
+
+
+Unset MetaRocq Strict Unquote Universe Mode.
+
+MetaRocq Run (_ <- define_ind;;
+                 define_fun).