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.mli | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

(limited to 'engine/evd.mli')

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