nf_relevance: also handle variables set above_prop

engine/eConstr.ml

@@ -35,7 +35,9 @@ module ESorts = struct
   let super sigma s =
     make (Sorts.super (kind sigma s))
 
-  let relevance_of_sort sigma s = Sorts.relevance_of_sort (kind sigma s)
+  let relevance_of_sort sigma s =
+    let r = Sorts.relevance_of_sort (unsafe_to_sorts s) in
+    UState.nf_relevance (Evd.evar_universe_context sigma) r
 
   let family sigma s = Sorts.family (kind sigma s)
 

engine/evarutil.ml

@@ -444,7 +444,7 @@ let new_evar ?src ?filter ?relevance ?abstract_arguments ?candidates ?(naming =
 
 let new_type_evar ?src ?filter ?naming ?principal ?hypnaming env evd rigid =
   let (evd', s) = new_sort_variable rigid evd in
-  let relevance = Sorts.relevance_of_sort (EConstr.ESorts.kind evd s) in
+  let relevance = EConstr.ESorts.relevance_of_sort evd s in
   let (evd', e) = new_evar env evd' ?src ?filter ~relevance ?naming ~typeclass_candidate:false ?principal ?hypnaming (EConstr.mkSort s) in
   evd', (e, s)
 

engine/uState.ml

@@ -35,6 +35,7 @@ module QState : sig
   val repr : elt -> t -> quality
   val set : elt -> quality -> t -> t option
   val set_above_prop : elt -> t -> t
+  val is_above_prop : elt -> t -> bool
   val collapse : t -> t
   val pr : t -> Pp.t
 end =
@@ -75,6 +76,8 @@ let rec repr q m = match QMap.find q m.qmap with
 (*   let () = assert !Flags.in_debugger in *) (* FIXME *)
   QVar q
 
+let is_above_prop q m = QSet.mem q m.above
+
 let set q qv m =
   let q = repr q m in
   let q = match q with QVar q -> q | QProp | QSProp | QType -> assert false in
@@ -313,7 +316,10 @@ let nf_relevance uctx r = match r with
   match nf_qvar uctx q with
   | QSProp -> Sorts.Irrelevant
   | QProp | QType -> Sorts.Relevant
-  | QVar q' -> if Sorts.QVar.equal q q' then r else Sorts.RelevanceVar q'
+  | QVar q' ->
+    if QState.is_above_prop q' uctx.sort_variables then Relevant
+    else if Sorts.QVar.equal q q' then r
+    else Sorts.RelevanceVar q'
 
 let nf_universes uctx c =
   let lsubst = uctx.univ_variables in

pretyping/retyping.ml

@@ -332,8 +332,8 @@ let relevance_of_term env sigma c =
 
 let relevance_of_type env sigma t =
   let s = get_sort_of env sigma t in
-  Sorts.relevance_of_sort (ESorts.kind sigma s)
+  ESorts.relevance_of_sort sigma s
 
-let relevance_of_sort s = Sorts.relevance_of_sort (EConstr.Unsafe.to_sorts s)
+let relevance_of_sort = ESorts.relevance_of_sort
 
-let relevance_of_sort_family f =  Sorts.relevance_of_sort_family f
+let relevance_of_sort_family sigma f = Evarutil.nf_relevance sigma (Sorts.relevance_of_sort_family f)

pretyping/retyping.mli

@@ -57,5 +57,5 @@ val print_retype_error : retype_error -> Pp.t
 
 val relevance_of_term : env -> evar_map -> constr -> Sorts.relevance
 val relevance_of_type : env -> evar_map -> types -> Sorts.relevance
-val relevance_of_sort : ESorts.t -> Sorts.relevance
-val relevance_of_sort_family : Sorts.family -> Sorts.relevance
+val relevance_of_sort : evar_map -> ESorts.t -> Sorts.relevance
+val relevance_of_sort_family : evar_map -> Sorts.family -> Sorts.relevance

pretyping/typing.ml

@@ -384,7 +384,7 @@ let warn_bad_relevance_binder ?loc env sigma rlv bnd = match CWarnings.get_statu
 let check_binder_relevance env sigma s decl =
   (* TODO: get rid of this *)
   let r = Evarutil.nf_relevance sigma (get_relevance decl) in
-  let r' = Sorts.relevance_of_sort (ESorts.kind sigma s) in
+  let r' = ESorts.relevance_of_sort sigma s in
   if Sorts.relevance_equal r' r then decl
   else begin
     warn_bad_relevance_binder env sigma r' decl;

vernac/comInductive.ml

@@ -129,7 +129,7 @@ let pretype_ind_arity env sigma (loc, c, impls, pseudo_poly) =
       | Some b -> Some (b, s)
       | None -> None
     in
-    sigma, (t, Retyping.relevance_of_sort s, concl, impls)
+    sigma, (t, Retyping.relevance_of_sort sigma s, concl, impls)
 
 (* ind_rel is the Rel for this inductive in the context without params.
    n is how many arguments there are in the constructor. *)