More backwards compatible pretyping of template

ppedrot · Jun 27, 2024 · 5bb9475 · 5bb9475
1 parent 304022a
commit 5bb9475
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 1 deletion.
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
@@ -1005,7 +1005,8 @@ struct
           | Some (Some u0 :: t, bound) ->
             (* template arg: type guaranteed to be syntactically an arity
                we replace the output universe with a fresh one *)
-            let sigma, u = Evd.new_univ_level_variable UState.univ_flexible_alg sigma in
+            (* rigid to get minimization to behave in a more backwards compatible way *)
+            let sigma, u = Evd.new_univ_level_variable UState.univ_rigid sigma in
             let s = ESorts.make @@ Sorts.sort_of_univ @@ Univ.Universe.make u in
             let ctx, _ = destArity sigma c1 in
             let bound =

diff --git a/test-suite/bugs/bug_19228_1.v b/test-suite/bugs/bug_19228_1.v
@@ -0,0 +1,7 @@
+Axiom invert_Some : forall {A} (x : option A),
+    match x with
+    | Some _ => A
+    | None => unit
+    end.
+(* A gets elaborated to Type on master but Set on this PR. *)
+Check @invert_Some Type.