From f011a88bd4be4797617741d6829d2530bc29ebdf Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 17 Jan 2020 17:28:50 +0100
Subject: schemes: use rigid universes

so for instance

~~~coq
Set Printing All. Set Printing Universes.

Polymorphic Inductive foo@{u v|u<=v} : Type@{u}:= .
Lemma bla@{u v|u < v} : foo@{u v} -> False.
Proof. induction 1. Qed.
~~~

works.
---
 tactics/elimschemes.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index d6fda00ad8..6cdb24965d 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -49,14 +49,14 @@ let optimize_non_type_induction_scheme kind dep sort ind =
     let sigma = Evd.minimize_universes sigma in
     (Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma)
   else
-    let sigma, pind = Evd.fresh_inductive_instance env sigma ind in
+    let sigma, pind = Evd.fresh_inductive_instance ~rigid:UState.univ_rigid env sigma ind in
     let sigma, c = build_induction_scheme env sigma pind dep sort in
       (c, Evd.evar_universe_context sigma)
 
 let build_induction_scheme_in_type dep sort ind =
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  let sigma, pind = Evd.fresh_inductive_instance env sigma ind in
+  let sigma, pind = Evd.fresh_inductive_instance ~rigid:UState.univ_rigid env sigma ind in
   let sigma, c = build_induction_scheme env sigma pind dep sort in
     c, Evd.evar_universe_context sigma
 
-- 
cgit v1.2.3