Fix relevance of domain in define_pure_evar_as_product.

Author: ppedrot

pretyping/evardefine.ml

@@ -83,7 +83,7 @@ let define_pure_evar_as_product env evd evk =
   let evd1,(dom,u1) =
     new_type_evar evenv evd univ_flexible_alg ~src ~filter:(evar_filter evi)
   in
-  let rdom = Sorts.Relevant in (* TODO relevance *)
+  let rdom = Sorts.relevance_of_sort (ESorts.kind evd1 u1) in
   let evd2,rng =
     let newenv = push_named (LocalAssum (make_annot id rdom, dom)) evenv in
     let src = subterm_source evk ~where:Codomain evksrc in