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.
---
 engine/evd.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index 8e7d942c37..70f58163fd 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -902,14 +902,14 @@ let make_nonalgebraic_variable evd u =
 let fresh_sort_in_family ?loc ?(rigid=univ_flexible) evd s =
   with_context_set ?loc rigid evd (UnivGen.fresh_sort_in_family s)
 
-let fresh_constant_instance ?loc env evd c =
-  with_context_set ?loc univ_flexible evd (UnivGen.fresh_constant_instance env c)
+let fresh_constant_instance ?loc ?(rigid=univ_flexible) env evd c =
+  with_context_set ?loc rigid evd (UnivGen.fresh_constant_instance env c)
 
-let fresh_inductive_instance ?loc env evd i =
-  with_context_set ?loc univ_flexible evd (UnivGen.fresh_inductive_instance env i)
+let fresh_inductive_instance ?loc ?(rigid=univ_flexible) env evd i =
+  with_context_set ?loc rigid evd (UnivGen.fresh_inductive_instance env i)
 
-let fresh_constructor_instance ?loc env evd c =
-  with_context_set ?loc univ_flexible evd (UnivGen.fresh_constructor_instance env c)
+let fresh_constructor_instance ?loc ?(rigid=univ_flexible) env evd c =
+  with_context_set ?loc rigid evd (UnivGen.fresh_constructor_instance env c)
 
 let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr =
   with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?loc ?names env gr)
-- 
cgit v1.2.3