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 ++++++------
 engine/evd.mli | 12 ++++++++----
 2 files changed, 14 insertions(+), 10 deletions(-)

(limited to 'engine')

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)
diff --git a/engine/evd.mli b/engine/evd.mli
index 8843adc853..82e1003a65 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -653,10 +653,14 @@ val update_sigma_env : evar_map -> env -> evar_map
 
 (** Polymorphic universes *)
 
-val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> evar_map -> Sorts.family -> evar_map * Sorts.t
-val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> Constant.t -> evar_map * pconstant
-val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> evar_map * pinductive
-val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor
+val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid
+  -> evar_map -> Sorts.family -> evar_map * Sorts.t
+val fresh_constant_instance : ?loc:Loc.t -> ?rigid:rigid
+  -> env -> evar_map -> Constant.t -> evar_map * pconstant
+val fresh_inductive_instance : ?loc:Loc.t -> ?rigid:rigid
+  -> env -> evar_map -> inductive -> evar_map * pinductive
+val fresh_constructor_instance : ?loc:Loc.t -> ?rigid:rigid
+  -> env -> evar_map -> constructor -> evar_map * pconstructor
 
 val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env ->
   evar_map -> GlobRef.t -> evar_map * econstr
-- 
cgit v1.2.3